------------------------------------------------------------------------
-- Up-to techniques for strong bisimilarity
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Up-to (lts : LTS) where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bisimilarity.Coinductive lts
import Bisimilarity.Coinductive.Equational-reasoning-instances
open import Equational-reasoning
open import Relation
import Up-to

open LTS lts

------------------------------------------------------------------------
-- The general up-to machinery, instantiated with the S̲t̲e̲p̲ container

open Up-to S̲t̲e̲p̲ public

------------------------------------------------------------------------
-- Some examples

-- Up to bisimilarity.

Up-to-bisimilarity : Trans₂ (# 0) Proc
Up-to-bisimilarity R = Bisimilarity   R  Bisimilarity 

-- Up to bisimilarity is monotone.

Up-to-bisimilarity-monotone : Monotone Up-to-bisimilarity
Up-to-bisimilarity-monotone R⊆S =
  Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))

-- Up to bisimilarity is size-preserving.
--
-- One can perhaps argue that the last part of this proof is less
-- complicated than Pous and Sangiorgi's proof of Lemma 6.3.13 in
-- "Enhancements of the bisimulation proof method". (Pous and
-- Sangiorgi seem to take for granted that the function is monotone.)

Up-to-bisimilarity-size-preserving : Size-preserving Up-to-bisimilarity
Up-to-bisimilarity-size-preserving =
  _⇔_.from (monotone→⇔ Up-to-bisimilarity-monotone)
     where
       {x = p , q} (r , p∼r , s , r∼s , s∼q) 
         p  ∼⟨ p∼r 
         r  ∼⟨ r∼s 
         s  ∼⟨ s∼q ⟩■
         q)

-- Up to union with bisimilarity.

Up-to-∪∼ : Trans₂ (# 0) Proc
Up-to-∪∼ R = R  Bisimilarity 

-- Up to union with bisimilarity is monotone.

Up-to-∪∼-monotone : Monotone Up-to-∪∼
Up-to-∪∼-monotone R⊆S = ⊎-map R⊆S id

-- Up to union with bisimilarity is size-preserving.
--
-- The proof is similar to parts of the proof of Pous and Sangiorgi's
-- Corollary 6.3.15.

Up-to-∪∼-size-preserving : Size-preserving Up-to-∪∼
Up-to-∪∼-size-preserving =
  ∪-closure
    id-size-preserving
    (const-size-preserving (Bisimilarity   ⊆⟨ id ⟩∎
                            Bisimilarity   ))

-- Up to transitive closure.

Up-to-* : Trans₂ (# 0) Proc
Up-to-* R = R *

-- Up to transitive closure is monotone.

Up-to-*-monotone : Monotone Up-to-*
Up-to-*-monotone R⊆S = Σ-map id  {n}  ^^-mono R⊆S n)
  where
  ^^-mono :  {R S}  R  S 
             n  R ^^ n  S ^^ n
  ^^-mono R⊆S zero    = id
  ^^-mono R⊆S (suc n) = Σ-map id (Σ-map R⊆S (^^-mono R⊆S n))

-- Up to transitive closure is size-preserving.

Up-to-*-size-preserving : Size-preserving Up-to-*
Up-to-*-size-preserving =
  _⇔_.from (monotone→⇔ Up-to-*-monotone) drop-*
  where
  drop-* :  {i}  Bisimilarity i *  Bisimilarity i
  drop-* {x = p , .p} (zero  , refl)           = p 
  drop-* {x = p , r}  (suc n , q , p∼q , ∼ⁿqr) =
    p  ∼⟨ p∼q 
    q  ∼⟨ drop-* (n , ∼ⁿqr) ⟩■
    r