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

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

open import Prelude

open import Labelled-transition-system

module Similarity.Equational-reasoning-instances
         {ℓ} {lts : LTS ℓ} {i : Size} where

open import Bisimilarity lts
open import Equational-reasoning
open import Similarity lts

instance

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

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

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

  convert≤′≤ : Convertible _≤′_ [ 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

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

  convert∼′≤ : 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) = ∼⇒≤ p∼q

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

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

  trans≤′≤ : Transitive _≤′_ [ 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)