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

{-# OPTIONS --without-K --safe --sized-types #-}

open import Prelude

open import Labelled-transition-system

module Similarity.Weak.Equational-reasoning-instances
         {} {lts : LTS } where

open import Bisimilarity lts
open import Bisimilarity.Weak lts
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
open import Expansion lts
import Expansion.Equational-reasoning-instances
open import Similarity lts
open import Similarity.Weak lts

instance

  reflexive≼ :  {i}  Reflexive [ i ]_≼_
  reflexive≼ = is-reflexive reflexive-≼

  reflexive≼′ :  {i}  Reflexive [ i ]_≼′_
  reflexive≼′ = is-reflexive reflexive-≼′

  convert≼≼ :  {i}  Convertible [ i ]_≼_ [ i ]_≼_
  convert≼≼ = is-convertible id

  convert≼′≼ :  {i}  Convertible _≼′_ [ i ]_≼_
  convert≼′≼ = is-convertible λ p≼′q  force p≼′q

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

  convert≼′≼′ :  {i}  Convertible [ i ]_≼′_ [ i ]_≼′_
  convert≼′≼′ = is-convertible id

  convert≤≼ :  {i}  Convertible [ i ]_≤_ [ i ]_≼_
  convert≤≼ = is-convertible ≤⇒≼

  convert≤′≼ :  {i}  Convertible _≤′_ [ i ]_≼_
  convert≤′≼ = is-convertible (convert  ≤⇒≼′)

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

  convert≤′≼′ :  {i}  Convertible [ i ]_≤′_ [ i ]_≼′_
  convert≤′≼′ = is-convertible ≤⇒≼′

  convert≈≼ :  {i}  Convertible [ i ]_≈_ [ i ]_≼_
  convert≈≼ = is-convertible ≈⇒≼

  convert≈′≼ :  {i}  Convertible _≈′_ [ i ]_≼_
  convert≈′≼ = is-convertible (convert  ≈⇒≼′)

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

  convert≈′≼′ :  {i}  Convertible [ i ]_≈′_ [ i ]_≼′_
  convert≈′≼′ = is-convertible ≈⇒≼′

  convert∼≼ :  {i}  Convertible [ i ]_∼_ [ i ]_≼_
  convert∼≼ = is-convertible (≈⇒≼  convert {a = })

  convert∼′≼ :  {i}  Convertible _∼′_ [ i ]_≼_
  convert∼′≼ = is-convertible (convert  ≈⇒≼′  convert {a = })

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

  convert∼′≼′ :  {i}  Convertible [ i ]_∼′_ [ i ]_≼′_
  convert∼′≼′ = is-convertible (≈⇒≼′  convert {a = })

  trans≼≼ :  {i}  Transitive′ [ i ]_≼_ _≼_
  trans≼≼ = is-transitive transitive-≼

  trans≼′≼ : Transitive′ _≼′_ _≼_
  trans≼′≼ = is-transitive transitive-≼′

  trans≼′≼′ :  {i}  Transitive′ [ i ]_≼′_ _≼′_
  trans≼′≼′ = is-transitive  p≼q  transitive-≼′ p≼q  convert)

  trans≼≼′ :  {i}  Transitive′ [ i ]_≼_ _≼′_
  trans≼≼′ = is-transitive  p≼q  transitive-≼ p≼q  convert)

  trans≳≼ :  {i}  Transitive [ i ]_≳_ [ i ]_≼_
  trans≳≼ = is-transitive transitive-≳≼

  trans≳′≼ :  {i}  Transitive _≳′_ [ i ]_≼_
  trans≳′≼ = is-transitive (transitive-≳≼  convert {a = })

  trans≳′≼′ :  {i}  Transitive [ i ]_≳′_ [ i ]_≼′_
  trans≳′≼′ = is-transitive transitive-≳≼′

  trans≳≼′ :  {i}  Transitive [ i ]_≳_ [ i ]_≼′_
  trans≳≼′ = is-transitive (transitive-≳≼′  convert {a = })