{-# OPTIONS --sized-types #-}
open import Prelude
open import Labelled-transition-system
module Bisimilarity.General
{ℓ}
(lts : LTS ℓ)
(open LTS lts)
(_[_]↝₁_ _[_]↝₂_ : Proc → Label → Proc → Type ℓ)
(⟶→↝₁ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝₁ q)
(⟶→↝₂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝₂ q)
where
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size
open import Bijection equality-with-J as Bijection using (_↔_)
open import Extensionality equality-with-J as Eq hiding (Extensionality)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Bisimilarity.Step lts _[_]↝₁_ _[_]↝₂_ as Step public
using (StepC)
open import Indexed-container hiding (⟨_⟩; Bisimilarity)
open import Indexed-container.Combinators hiding (id; _∘_)
open import Relation
import Similarity.Step lts _[_]↝₁_ as Step₁
import Similarity.Step lts _[_]↝₂_ as Step₂
open Indexed-container public using (force)
infix 4 _∼_ _∼′_ [_]_∼_ [_]_∼′_
Bisimilarity : Size → Rel₂ ℓ Proc
Bisimilarity = ν StepC
Bisimilarity′ : Size → Rel₂ ℓ Proc
Bisimilarity′ = ν′ StepC
[_]_∼_ : Size → Proc → Proc → Type ℓ
[_]_∼_ i = curry (Bisimilarity i)
[_]_∼′_ : Size → Proc → Proc → Type ℓ
[_]_∼′_ i = curry (Bisimilarity′ i)
_∼_ : Proc → Proc → Type ℓ
_∼_ = [ ∞ ]_∼_
_∼′_ : Proc → Proc → Type ℓ
_∼′_ = [ ∞ ]_∼′_
mutual
reflexive-∼ : ∀ {p i} → [ i ] p ∼ p
reflexive-∼ =
StepC.⟨ (λ p⟶p′ → _ , ⟶→↝₁ p⟶p′ , reflexive-∼′)
, (λ q⟶q′ → _ , ⟶→↝₂ q⟶q′ , reflexive-∼′)
⟩
reflexive-∼′ : ∀ {p i} → [ i ] p ∼′ p
force reflexive-∼′ = reflexive-∼
≡⇒∼ : ∀ {p q} → p ≡ q → p ∼ q
≡⇒∼ refl = reflexive-∼
infix -2 ∼:_ ∼′:_
∼:_ : ∀ {i p q} → [ i ] p ∼ q → [ i ] p ∼ q
∼:_ = id
∼′:_ : ∀ {i p q} → [ i ] p ∼′ q → [ i ] p ∼′ q
∼′:_ = id
infix 4 [_]_≡_ [_]_≡′_
[_]_≡_ : ∀ {p q} → Size → (_ _ : ν StepC ∞ (p , q)) → Type ℓ
[_]_≡_ i = curry (ν-bisimilar i)
[_]_≡′_ : ∀ {p q} → Size → (_ _ : ν′ StepC ∞ (p , q)) → Type ℓ
[_]_≡′_ i = curry (ν′-bisimilar i)
[]≡↔ :
Eq.Extensionality ℓ ℓ →
∀ {p q} {i : Size} (p∼q₁ p∼q₂ : ν StepC ∞ (p , q)) →
[ i ] p∼q₁ ≡ p∼q₂
↔
(∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
×
(∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)
[]≡↔ ext {p} {q} {i} p∼q₁@(s₁ , f₁) p∼q₂@(s₂ , f₂) =
[ i ] p∼q₁ ≡ p∼q₂ ↝⟨ ν-bisimilar↔ ext p∼q₁ p∼q₂ ⟩
⟦ StepC₁ ⟷ StepC₂ ⟧₂ (ν′-bisimilar i) (p∼q₁ , p∼q₂) ↝⟨ ⟦⟷⟧₂↔ ext StepC₁ StepC₂ (ν′-bisimilar i) p∼q₁ p∼q₂ ⟩
⟦ StepC₁ ⟧₂ (ν′-bisimilar i)
((proj₁ s₁ , f₁ ∘ inj₁) , (proj₁ s₂ , f₂ ∘ inj₁))
×
⟦ StepC₂ ⟧₂ (ν′-bisimilar i)
( (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p)))
, (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p)))
) ↝⟨ Step₁.⟦StepC⟧₂↔ ext (ν′-bisimilar i) (proj₁ s₁ , f₁ ∘ inj₁)
(proj₁ s₂ , f₂ ∘ inj₁)
×-cong
Step₂.⟦StepC⟧₂↔ ext (ν′-bisimilar i)
(proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p)))
(proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p))) ⟩
(∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
let q′₁ , q⟶q′₁ , p′∼q′₁ =
Step₁.StepC.challenge (proj₁ s₁ , f₁ ∘ inj₁) p⟶p′
q′₂ , q⟶q′₂ , p′∼q′₂ =
Step₁.StepC.challenge (proj₁ s₂ , f₂ ∘ inj₁) p⟶p′
in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
×
((∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
let p′₁ , p⟶p′₁ , p′∼q′₁ =
Step₂.StepC.challenge
(proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p))) q⟶q′
p′₂ , p⟶p′₂ , p′∼q′₂ =
Step₂.StepC.challenge
(proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p))) q⟶q′
in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)) ↔⟨⟩
(∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
×
(∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂) □
where
open Container
StepC₁ = Step₁.StepC
StepC₂ = Step₂.StepC
module Bisimilarity-of-∼
(ext : Eq.Extensionality ℓ ℓ)
{p q} {i : Size}
(p∼q₁ p∼q₂ : ν StepC ∞ (p , q))
where
⟨_,_,_,_,_⟩ :
(∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂) →
(∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂) →
[ i ] p∼q₁ ≡ p∼q₂
⟨_,_,_,_,_⟩ = curry (_↔_.from ([]≡↔ ext p∼q₁ p∼q₂))
left-to-right :
[ i ] p∼q₁ ≡ p∼q₂ →
∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂
left-to-right = proj₁ ∘ _↔_.to ([]≡↔ ext p∼q₁ p∼q₂)
right-to-left :
[ i ] p∼q₁ ≡ p∼q₂ →
∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
×
[ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂
right-to-left = proj₂ ∘ _↔_.to ([]≡↔ ext p∼q₁ p∼q₂)
Extensionality : Type ℓ
Extensionality = ν′-extensionality StepC
extensionality :
Eq.Extensionality ℓ ℓ →
Extensionality →
∀ {p q} {p∼q₁ p∼q₂ : ν StepC ∞ (p , q)} →
[ ∞ ] p∼q₁ ≡ p∼q₂ → p∼q₁ ≡ p∼q₂
extensionality ext ν-ext = ν-extensionality ext ν-ext
open StepC public using (⟨_,_⟩; left-to-right; right-to-left)