------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Prelude

open import Labelled-transition-system

module Bisimilarity.Coinductive.Equational-reasoning-instances
         {lts : LTS} {i : Size} where

open import Bisimilarity.Coinductive lts
open import Equational-reasoning

instance

  reflexive∼ : Reflexive [ i ]_∼_
  reflexive∼ = is-reflexive reflexive-∼

  reflexive∼′ : Reflexive [ i ]_∼′_
  reflexive∼′ = is-reflexive reflexive-∼′

  symmetric∼ : Symmetric [ i ]_∼_
  symmetric∼ = is-symmetric symmetric-∼

  symmetric∼′ : Symmetric [ i ]_∼′_
  symmetric∼′ = is-symmetric symmetric-∼′

  trans∼∼ : Transitive [ i ]_∼_ [ i ]_∼_
  trans∼∼ = is-transitive transitive-∼

  trans∼′∼ : Transitive [ ssuc i ]_∼′_ [ i ]_∼_
  trans∼′∼ = is-transitive λ p∼′q  transitive (force p∼′q)

  trans∼′∼′ : Transitive [ i ]_∼′_ [ i ]_∼′_
  trans∼′∼′ = is-transitive transitive-∼′

  trans∼∼′ : Transitive [ i ]_∼_ [ i ]_∼′_
  trans∼∼′ = is-transitive lemma
    where
    lemma :  {p q r}  [ i ] p  q  [ i ] q ∼′ r  [ i ] p ∼′ r
    force (lemma p∼q q∼′r) = transitive-∼ p∼q (force q∼′r)

  convert∼∼ : Convertible [ i ]_∼_ [ i ]_∼_
  convert∼∼ = is-convertible id

  convert∼′∼ : Convertible [ ssuc i ]_∼′_ [ i ]_∼_
  convert∼′∼ = is-convertible λ p∼′q  force p∼′q

  convert∼∼′ : Convertible [ i ]_∼_ [ i ]_∼′_
  convert∼∼′ = is-convertible lemma
    where
    lemma :  {p q}  [ i ] p  q  [ i ] p ∼′ q
    force (lemma p∼q) = p∼q

  convert∼′∼′ : Convertible [ i ]_∼′_ [ i ]_∼′_
  convert∼′∼′ = is-convertible id