```------------------------------------------------------------------------
-- Up-to techniques for the standard coinductive definition of weak
-- bisimilarity
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Weak.Up-to {ℓ} (lts : LTS ℓ) where

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bisimilarity.Weak lts
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
open import Expansion lts as E using (Expansion; _≲_; ≳:_)
import Expansion.Equational-reasoning-instances
open import Indexed-container
open import Relation
import Similarity.Weak lts as S
import Up-to

open LTS lts

import Similarity.Step lts _[_]⇒̂_ as SS

------------------------------------------------------------------------
-- The general up-to machinery, instantiated with the StepC container

open Up-to StepC public

------------------------------------------------------------------------
-- Up to expansion

-- Up to expansion.
--
-- I took this definition from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi.

Up-to-expansion : Trans₂ ℓ Proc
Up-to-expansion R = Expansion ∞ ⊙ R ⊙ Expansion ∞ ⁻¹

-- Up to expansion is monotone.

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

-- Up to expansion is size-preserving.

up-to-expansion-size-preserving : Size-preserving Up-to-expansion
up-to-expansion-size-preserving =
_⇔_.from (monotone→⇔ up-to-expansion-monotone)
(λ where
{x = p , q} (r , p≳r , s , r≈s , s≲q) →
p  ∼⟨ p≳r ⟩
r  ∼′⟨ r≈s ⟩ ≳:
s  ∽⟨ s≲q ⟩■
q)

------------------------------------------------------------------------
-- A generalisation of up to expansion

mutual

-- A monolithic implementation of a non-symmetric variant of up to
-- expansion, based on the technique presented in Section 6.5.2.4 of
-- "Enhancements of the bisimulation proof method" by Pous and
-- Sangiorgi.
--
-- It is at the time of writing not clear to me if there is some
-- size-preserving proof that matches this technique.

6-5-2-4 :
{R : Rel₂ ℓ Proc} →
(∀ {P P′ Q μ} →
R (P , Q) → P [ μ ]⟶ P′ →
∃ λ Q′ → Q [ μ ]⇒̂ Q′ ×
(Expansion ∞ ⊙ R ⊙ Weak-bisimilarity ∞) (P′ , Q′)) →
(∀ {P Q Q′ μ} →
R (P , Q) → Q [ μ ]⟶ Q′ →
∃ λ P′ → P [ μ ]⇒̂ P′ ×
(Weak-bisimilarity ∞ ⊙ R ⊙ Expansion ∞ ⁻¹) (P′ , Q′)) →
R ⊆ Weak-bisimilarity ∞
6-5-2-4 {R} lr⟶ rl⟶ =
6-5-2-4′ (λ PRQ → S.⟨ lr⟶ PRQ ⟩)
(λ PR⁻¹Q → S.⟨ Σ-map id (Σ-map id lemma) ∘ rl⟶ PR⁻¹Q ⟩)
where
lemma :
Weak-bisimilarity ∞ ⊙ R ⊙ Expansion ∞ ⁻¹ ⊆
(Expansion ∞ ⊙ R ⁻¹ ⊙ Weak-bisimilarity ∞) ⁻¹
lemma (_ , P₁≈P₂ , _ , P₂RP₃ , P₃≲P₄) =
(_ , P₃≲P₄ , _ , P₂RP₃ , symmetric P₁≈P₂)

-- A variant of 6-5-2-4.

6-5-2-4′ :
let Prog = λ (R : Rel₂ ℓ Proc) →
R ⊆ ⟦ S.StepC ⟧ (Expansion ∞ ⊙ R ⊙ Weak-bisimilarity ∞) in
∀ {R} → Prog R → Prog (R ⁻¹) → R ⊆ Weak-bisimilarity ∞
6-5-2-4′ {R} lr⟶ rl⟶ =
R                    ⊆⟨ ⊆≈≈ ⟩
≈ R ≈                ⊆⟨ unfold _ (λ P≈R≈Q →
StepC.⟨ SS.Step.challenge (lemma lr⟶ P≈R≈Q)
, Σ-map id (Σ-map id ≈≈-sym) ∘
SS.Step.challenge (lemma rl⟶ (≈≈-sym P≈R≈Q))
⟩) ⟩∎
Weak-bisimilarity ∞  ∎
where
≈_≈ : Rel₂ ℓ Proc → Rel₂ ℓ Proc
≈ R ≈ = Weak-bisimilarity ∞ ⊙ R ⊙ Weak-bisimilarity ∞

⊆≈≈ : ∀ {R} → R ⊆ ≈ R ≈
⊆≈≈ r = _ , reflexive , _ , r , reflexive

≳_≈ : Rel₂ ℓ Proc → Rel₂ ℓ Proc
≳ R ≈ = Expansion ∞ ⊙ R ⊙ Weak-bisimilarity ∞

⊆≳≈ : ∀ {R} → R ⊆ ≳ R ≈
⊆≳≈ r = _ , reflexive , _ , r , reflexive

≈≈-sym : ∀ {R} → ≈ R ≈ ⊆ ≈ R ⁻¹ ≈ ⁻¹
≈≈-sym (_ , P₁≈P₂ , _ , P₂RP₃ , P₃≈P₄) =
(_ , symmetric P₃≈P₄ , _ , P₂RP₃ , symmetric P₁≈P₂)

lemma : ∀ {R} → R ⊆ ⟦ S.StepC ⟧ ≳ R ≈ → ≈ R ≈ ⊆ SS.Step ≈ R ≈
lemma {R} lr⟶ = λ where
(P₁ , P≈P₁ , Q₁ , P₁RQ₁ , Q₁≈Q) .SS.Step.challenge P⟶P₁ →
let P₁′ , P₁⟶̂P₁′ , P′≈′P₁′ = left-to-right P≈P₁ P⟶P₁
Q₁′ , Q₁⇒̂Q₁′ , P₁″ ,
P₁′≳P₁″ , Q₁″ ,
P₁″RQ₁″ , Q₁″≈Q₁′    = lr≳≈⇒̂ (⊆≳≈ P₁RQ₁) P₁⟶̂P₁′
Q′ , Q⇒̂Q′  , Q₁′≈Q′    = weak-is-weak⇒̂ Q₁≈Q Q₁⇒̂Q₁′
in Q′ , Q⇒̂Q′ , P₁″
, transitive′ {a = ℓ} (force P′≈′P₁′) P₁′≳P₁″
, Q₁″ , P₁″RQ₁″ , transitive {a = ℓ} Q₁″≈Q₁′ Q₁′≈Q′
where
lr⟶̂ :
∀ {P P′ Q μ} →
R (P , Q) → P [ μ ]⟶̂ P′ → ∃ λ Q′ → Q [ μ ]⇒̂ Q′ × ≳ R ≈ (P′ , Q′)
lr⟶̂ PRQ (done s)    = _ , silent s done , ⊆≳≈ PRQ
lr⟶̂ PRQ (step P⟶P′) = S.challenge (lr⟶ PRQ) P⟶P′

lr≳≈⟶ :
∀ {P P′ Q μ} →
≳ R ≈ (P , Q) → P [ μ ]⟶ P′ →
∃ λ Q′ → Q [ μ ]⇒̂ Q′ × ≳ R ≈ (P′ , Q′)
lr≳≈⟶ (P₁ , P≳P₁ , Q₁ , P₁RQ₁ , Q₁≈Q) P⟶P′ =
let P₁′ , P₁⟶̂P₁′ , P′≳P₁′          = E.left-to-right P≳P₁ P⟶P′
Q₁′ , Q₁⇒̂Q₁′ , P₁″ , P₁′≳P₁″ ,
Q₁″ , P₁″RQ₁″ , Q₁″≈Q₁′      = lr⟶̂ P₁RQ₁ P₁⟶̂P₁′
Q′ , Q⇒̂Q′ , Q₁′≈Q′             = weak-is-weak⇒̂ Q₁≈Q Q₁⇒̂Q₁′
in Q′ , Q⇒̂Q′ ,
P₁″ , transitive {a = ℓ} P′≳P₁′ P₁′≳P₁″ ,
Q₁″ , P₁″RQ₁″ , transitive {a = ℓ} Q₁″≈Q₁′ Q₁′≈Q′

lr≳≈⇒ :
∀ {P P′ Q} →
≳ R ≈ (P , Q) → P ⇒ P′ → ∃ λ Q′ → Q ⇒ Q′ × ≳ R ≈ (P′ , Q′)
lr≳≈⇒ P≳R≈Q done                = _ , done , P≳R≈Q
lr≳≈⇒ P≳R≈Q (step s P⟶P′ P′⇒P″) =
let Q′ , Q⇒̂Q′  , P′≳R≈Q′ = lr≳≈⟶ P≳R≈Q P⟶P′
Q″ , Q′⇒Q″ , P″≳R≈Q″ = lr≳≈⇒ P′≳R≈Q′ P′⇒P″
in Q″ , ⇒-transitive (⇒̂→⇒ s Q⇒̂Q′) Q′⇒Q″ , P″≳R≈Q″

lr≳≈[]⇒ :
∀ {P P′ Q μ} →
¬ Silent μ →
≳ R ≈ (P , Q) → P [ μ ]⇒ P′ →
∃ λ Q′ → Q [ μ ]⇒ Q′ × ≳ R ≈ (P′ , Q′)
lr≳≈[]⇒ ¬s P≳R≈Q (steps P⇒P′ P′⟶P″ P″⇒P‴) =
let Q′ , Q⇒Q′  , P′≳R≈Q′ = lr≳≈⇒ P≳R≈Q P⇒P′
Q″ , Q′⇒̂Q″ , P″≳R≈Q″ = lr≳≈⟶ P′≳R≈Q′ P′⟶P″
Q‴ , Q″⇒Q‴ , P‴≳R≈Q‴ = lr≳≈⇒ P″≳R≈Q″ P″⇒P‴
in Q‴
, []⇒⇒-transitive (⇒[]⇒-transitive Q⇒Q′ (⇒̂→[]⇒ ¬s Q′⇒̂Q″)) Q″⇒Q‴
, P‴≳R≈Q‴

lr≳≈⇒̂ :
∀ {P P′ Q μ} →
≳ R ≈ (P , Q) → P [ μ ]⇒̂ P′ →
∃ λ Q′ → Q [ μ ]⇒̂ Q′ × ≳ R ≈ (P′ , Q′)
lr≳≈⇒̂ PRQ = λ where
(silent s P⇒P′)      → Σ-map id (Σ-map (silent s)      id)
(lr≳≈⇒ PRQ P⇒P′)
(non-silent ¬s P⇒P′) → Σ-map id (Σ-map (non-silent ¬s) id)
(lr≳≈[]⇒ ¬s PRQ P⇒P′)

------------------------------------------------------------------------
-- Up to weak bisimilarity

-- Up to weak bisimilarity.
--
-- I based this definition on Definition 4.2.13 in Milner's
-- "Operational and Algebraic Semantics of Concurrent Processes".

Up-to-weak-bisimilarity : Trans₂ ℓ Proc
Up-to-weak-bisimilarity R =
Weak-bisimilarity ∞ ⊙ R ⊙ Weak-bisimilarity ∞

-- Up to weak bisimilarity is monotone.

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

-- If transitivity of weak bisimilarity is size-preserving in the
-- first argument, then "up to weak bisimilarity" is size-preserving.

size-preserving-transitivity→up-to-weak-bisimilarity-size-preserving :
(∀ {i x y z} → [ i ] x ≈ y → [ ∞ ] y ≈ z → [ i ] x ≈ z) →
Size-preserving Up-to-weak-bisimilarity
size-preserving-transitivity→up-to-weak-bisimilarity-size-preserving
trans =
_⇔_.from (monotone→⇔ up-to-weak-bisimilarity-monotone) λ where
{x = p , q} (r , p≈r , s , r≈s , s≈q) →
p  ≈∞⟨ p≈r ⟩
r  ≈⟨ r≈s ⟩∞
s  ∼⟨ s≈q ⟩■
q
where
infixr -2 _≈⟨_⟩∞_ _≈∞⟨_⟩_

_≈⟨_⟩∞_ : ∀ {i} x {y z} → [ i ] x ≈ y → [ ∞ ] y ≈ z → [ i ] x ≈ z
_ ≈⟨ p ⟩∞ q = trans p q

_≈∞⟨_⟩_ : ∀ {i} x {y z} → [ ∞ ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z
_ ≈∞⟨ p ⟩ q = symmetric (trans (symmetric q) (symmetric p))

-- If transitivity of weak bisimilarity is size-preserving in both
-- arguments, then weak bisimulations up to weak bisimilarity are
-- contained in weak bisimilarity.

size-preserving-transitivity→up-to-weak-bisimilarity-up-to :
(∀ {i x y z} → [ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z) →
Up-to-technique Up-to-weak-bisimilarity
size-preserving-transitivity→up-to-weak-bisimilarity-up-to =
size-preserving→up-to ∘
size-preserving-transitivity→up-to-weak-bisimilarity-size-preserving
```