{-# OPTIONS --sized-types #-}
open import Prelude
module Bisimilarity.CCS {ℓ} {Name : Type ℓ} where
open import Equality.Propositional
open import Prelude.Size
import Bisimilarity.Equational-reasoning-instances as I
import Bisimilarity.CCS.General
open import Equational-reasoning
open import Labelled-transition-system.CCS Name
open import Bisimilarity CCS
import Labelled-transition-system.Equational-reasoning-instances CCS
as Dummy
module Cong-lemmas
({R} R′ : Proc ∞ → Proc ∞ → Type ℓ)
⦃ _ : Convertible R R′ ⦄
⦃ _ : Convertible R′ R′ ⦄
⦃ _ : Convertible _∼_ R′ ⦄
⦃ _ : Transitive R′ R′ ⦄
(left-to-right :
∀ {P Q} → R P Q →
∀ {P′ μ} → P [ μ ]⟶ P′ → ∃ λ Q′ → Q [ μ ]⟶ Q′ × R′ P′ Q′)
where
private
infix -2 R′:_
R′:_ : ∀ {P Q} → R′ P Q → R′ P Q
R′:_ = id
infix -3 lr-result
lr-result :
∀ {P′ Q Q′} μ → R′ P′ Q′ → Q [ μ ]⟶ Q′ →
∃ λ Q′ → Q [ μ ]⟶ Q′ × R′ P′ Q′
lr-result _ P′∼′Q′ Q⟶Q′ = _ , Q⟶Q′ , P′∼′Q′
syntax lr-result μ P′∼′Q′ Q⟶Q′ = P′∼′Q′ [ μ ]⟵ Q⟶Q′
∣-cong :
(∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
∀ {P₁ P₂ Q₁ Q₂ S₁ μ} →
R P₁ P₂ → R Q₁ Q₂ → P₁ ∣ Q₁ [ μ ]⟶ S₁ →
∃ λ S₂ → P₂ ∣ Q₂ [ μ ]⟶ S₂ × R′ S₁ S₂
∣-cong _∣-cong′_ P₁∼P₂ Q₁∼Q₂ = λ where
(par-left tr) → Σ-map (_∣ _)
(Σ-map par-left
(_∣-cong′ convert Q₁∼Q₂))
(left-to-right P₁∼P₂ tr)
(par-right tr) → Σ-map (_ ∣_)
(Σ-map par-right
(convert P₁∼P₂ ∣-cong′_))
(left-to-right Q₁∼Q₂ tr)
(par-τ tr₁ tr₂) → Σ-zip _∣_ (Σ-zip par-τ _∣-cong′_)
(left-to-right P₁∼P₂ tr₁)
(left-to-right Q₁∼Q₂ tr₂)
⊕-cong :
∀ {P₁ P₁′ P₂ P₂′ S μ} →
R P₁ P₁′ → R P₂ P₂′ → P₁ ⊕ P₂ [ μ ]⟶ S →
∃ λ S′ → P₁′ ⊕ P₂′ [ μ ]⟶ S′ × R′ S S′
⊕-cong {P₁} {P₁′} {P₂} {P₂′} {S} {μ} P₁∼P₁′ P₂∼P₂′ = λ where
(sum-left P₁⟶S) → case left-to-right P₁∼P₁′ P₁⟶S of λ where
(S′ , P₁′⟶S′ , S∼′S′) →
S ∼⟨ S∼′S′ ⟩■
S′
[ μ ]⟵ ←⟨ ⟶: sum-left P₁′⟶S′ ⟩■
P₁′ ⊕ P₂′
(sum-right P₂⟶S) → case left-to-right P₂∼P₂′ P₂⟶S of λ where
(S′ , P₂′⟶S′ , S∼′S′) →
S ∼⟨ S∼′S′ ⟩■
S′
[ μ ]⟵ ←⟨ ⟶: sum-right P₂′⟶S′ ⟩■
P₁′ ⊕ P₂′
·-cong :
∀ {P₁ P₂ Q₁ μ μ′} →
R′ (force P₁) (force P₂) → μ · P₁ [ μ′ ]⟶ Q₁ →
∃ λ Q₂ → μ · P₂ [ μ′ ]⟶ Q₂ × R′ Q₁ Q₂
·-cong {P₁} {P₂} {μ = μ} P₁∼P₂ action =
force P₁ ∼⟨ P₁∼P₂ ⟩■
force P₂
[ μ ]⟵ ←⟨ ⟶: action ⟩■
μ · P₂
⟨ν⟩-cong :
(∀ {a P P′} → R′ P P′ → R′ (⟨ν a ⟩ P) (⟨ν a ⟩ P′)) →
∀ {a μ P P′ Q} →
R P P′ → ⟨ν a ⟩ P [ μ ]⟶ Q →
∃ λ Q′ → ⟨ν a ⟩ P′ [ μ ]⟶ Q′ × R′ Q Q′
⟨ν⟩-cong ⟨ν⟩-cong′ {a} {μ} {P′ = P′} P∼P′
(restriction {P′ = Q} a∉μ P⟶Q) =
case left-to-right P∼P′ P⟶Q of λ where
(Q′ , P′⟶Q′ , Q∼′Q′) →
⟨ν a ⟩ Q ∼⟨ ⟨ν⟩-cong′ Q∼′Q′ ⟩■
⟨ν a ⟩ Q′
[ μ ]⟵ ←⟨ ⟶: restriction a∉μ P′⟶Q′ ⟩■
⟨ν a ⟩ P′
!-cong :
(∀ {μ P P₀} →
! P [ μ ]⟶ P₀ →
(∃ λ P′ → P [ μ ]⟶ P′ × P₀ ∼ ! P ∣ P′)
⊎
(μ ≡ τ × ∃ λ P′ → ∃ λ P″ → ∃ λ a →
P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ ×
P₀ ∼ (! P ∣ P′) ∣ P″)) →
(∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
(∀ {P P′} → R′ P P′ → R′ (! P) (! P′)) →
∀ {P P′ Q μ} →
R P P′ → ! P [ μ ]⟶ Q →
∃ λ Q′ → ! P′ [ μ ]⟶ Q′ × R′ Q Q′
!-cong 6-1-3-2 _∣-cong′_ !-cong′_ {P} {P′} {Q} {μ} P∼P′ !P⟶Q =
case 6-1-3-2 !P⟶Q of λ where
(inj₁ (P″ , P⟶P″ , Q∼!P∣P″)) →
let Q′ , P′⟶Q′ , P″∼′Q′ = left-to-right P∼P′ P⟶P″
in
Q ∼⟨ R′: convert Q∼!P∣P″ ⟩
! P ∣ P″ ∼⟨ (!-cong′ convert P∼P′) ∣-cong′ P″∼′Q′ ⟩■
! P′ ∣ Q′
[ μ ]⟵ ←⟨ ⟶: replication (par-right P′⟶Q′) ⟩■
! P′
(inj₂ (refl , P″ , P‴ , a , P⟶P″ , P⟶P‴ , Q∼!P∣P″∣P‴)) →
let Q′ , P′⟶Q′ , P″∼′Q′ = left-to-right P∼P′ P⟶P″
Q″ , P′⟶Q″ , P‴∼′Q″ = left-to-right P∼P′ P⟶P‴
in
Q ∼⟨ R′: convert Q∼!P∣P″∣P‴ ⟩
(! P ∣ P″) ∣ P‴ ∼⟨ ((!-cong′ convert P∼P′) ∣-cong′ P″∼′Q′) ∣-cong′ P‴∼′Q″ ⟩■
(! P′ ∣ Q′) ∣ Q″
[ τ ]⟵ ←⟨ ⟶: replication (par-τ (replication (par-right P′⟶Q′)) P′⟶Q″) ⟩■
! P′
private
module CL {i} =
Cong-lemmas
[ i ]_∼′_
⦃ I.convert∼∼′ {i = i} ⦄
⦃ I.convert∼′∼′ {i = i} ⦄
⦃ I.convert∼∼′ {i = i} ⦄
left-to-right
mutual
∣-comm : ∀ {P Q i} → [ i ] P ∣ Q ∼ Q ∣ P
∣-comm {i = i} = ⟨ lr , Σ-map id (Σ-map id symmetric) ∘ lr ⟩
where
lr : ∀ {P P′ Q μ} →
P ∣ Q [ μ ]⟶ P′ →
∃ λ Q′ → Q ∣ P [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
lr (par-left tr) = _ , par-right tr , ∣-comm′
lr (par-right tr) = _ , par-left tr , ∣-comm′
lr (par-τ tr₁ tr₂) =
_
, par-τ tr₂ (subst (λ a → _ [ name a ]⟶ _)
(sym $ co-involutive _)
tr₁)
, ∣-comm′
∣-comm′ : ∀ {P Q i} → [ i ] P ∣ Q ∼′ Q ∣ P
force ∣-comm′ = ∣-comm
mutual
∣-assoc : ∀ {P Q R i} → [ i ] P ∣ (Q ∣ R) ∼ (P ∣ Q) ∣ R
∣-assoc {i = i} = ⟨ lr , rl ⟩
where
lr : ∀ {P Q R P′ μ} →
P ∣ (Q ∣ R) [ μ ]⟶ P′ →
∃ λ Q′ → (P ∣ Q) ∣ R [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
lr (par-left tr) = _ , par-left (par-left tr) , ∣-assoc′
lr (par-right (par-left tr)) = _ , par-left (par-right tr) , ∣-assoc′
lr (par-right (par-right tr)) = _ , par-right tr , ∣-assoc′
lr (par-right (par-τ tr₁ tr₂)) = _ , par-τ (par-right tr₁) tr₂ , ∣-assoc′
lr (par-τ tr₁ (par-left tr₂)) = _ , par-left (par-τ tr₁ tr₂) , ∣-assoc′
lr (par-τ tr₁ (par-right tr₂)) = _ , par-τ (par-left tr₁) tr₂ , ∣-assoc′
rl : ∀ {P Q R Q′ μ} →
(P ∣ Q) ∣ R [ μ ]⟶ Q′ →
∃ λ P′ → P ∣ (Q ∣ R) [ μ ]⟶ P′ × [ i ] P′ ∼′ Q′
rl (par-left (par-left tr)) = _ , par-left tr , ∣-assoc′
rl (par-left (par-right tr)) = _ , par-right (par-left tr) , ∣-assoc′
rl (par-left (par-τ tr₁ tr₂)) = _ , par-τ tr₁ (par-left tr₂) , ∣-assoc′
rl (par-right tr) = _ , par-right (par-right tr) , ∣-assoc′
rl (par-τ (par-left tr₁) tr₂) = _ , par-τ tr₁ (par-right tr₂) , ∣-assoc′
rl (par-τ (par-right tr₁) tr₂) = _ , par-right (par-τ tr₁ tr₂) , ∣-assoc′
∣-assoc′ : ∀ {P Q R i} → [ i ] P ∣ (Q ∣ R) ∼′ (P ∣ Q) ∣ R
force ∣-assoc′ = ∣-assoc
∣-left-identity : ∀ {i P} → [ i ] ∅ ∣ P ∼ P
∣-left-identity =
⟨ (λ { (par-right tr) → (_ , tr , λ { .force → ∣-left-identity })
; (par-left ())
; (par-τ () _)
})
, (λ tr → (_ , par-right tr , λ { .force → ∣-left-identity }))
⟩
∣-left-identity′ : ∀ {P i} → [ i ] ∅ ∣ P ∼′ P
force ∣-left-identity′ = ∣-left-identity
∣-right-identity : ∀ {P} → P ∣ ∅ ∼ P
∣-right-identity {P} =
P ∣ ∅ ∼⟨ ∣-comm ⟩
∅ ∣ P ∼⟨ ∣-left-identity ⟩■
P
mutual
infix 6 _∣-cong_ _∣-cong′_
_∣-cong_ : ∀ {i P P′ Q Q′} →
[ i ] P ∼ Q → [ i ] P′ ∼ Q′ → [ i ] P ∣ P′ ∼ Q ∣ Q′
P∼Q ∣-cong P′∼Q′ =
⟨ lr P∼Q P′∼Q′
, Σ-map id (Σ-map id symmetric) ∘
lr (symmetric P∼Q) (symmetric P′∼Q′)
⟩
where
lr = CL.∣-cong _∣-cong′_
_∣-cong′_ : ∀ {i P P′ Q Q′} →
[ i ] P ∼′ Q → [ i ] P′ ∼′ Q′ → [ i ] P ∣ P′ ∼′ Q ∣ Q′
force (P∼P′ ∣-cong′ Q∼Q′) = force P∼P′ ∣-cong force Q∼Q′
infix 6 _∣-congP_
_∣-congP_ : ∀ {i P P′ Q Q′} →
[ i ] P ∼ Q → [ i ] P′ ∼ Q′ → [ i ] P ∣ P′ ∼ Q ∣ Q′
_∣-congP_ {i} = λ p q →
⟨ lr p q
, Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p) (symmetric q)
⟩
where
lr : ∀ {P P′ P″ Q Q′ μ} →
[ i ] P ∼ Q → [ i ] P′ ∼ Q′ → P ∣ P′ [ μ ]⟶ P″ →
∃ λ Q″ → Q ∣ Q′ [ μ ]⟶ Q″ × [ i ] P″ ∼′ Q″
lr p q (par-left tr) =
let (_ , tr′ , p′) = left-to-right p tr
in (_ , par-left tr′ , λ { .force → force p′ ∣-congP q })
lr p q (par-right tr) =
let (_ , tr′ , q′) = left-to-right q tr
in (_ , par-right tr′ , λ { .force → p ∣-congP force q′ })
lr p q (par-τ tr₁ tr₂) =
let (_ , tr₁′ , p′) = left-to-right p tr₁
(_ , tr₂′ , q′) = left-to-right q tr₂
in (_ , par-τ tr₁′ tr₂′ , λ { .force → force p′ ∣-congP force q′ })
private
6-1-2-compact : ∀ {P i} → [ i ] ! P ∣ P ∼ ! P
6-1-2-compact =
⟨ (λ tr → _ , replication tr , reflexive)
, (λ { (replication tr) → _ , tr , reflexive })
⟩
6-1-2 : ∀ {P i} → [ i ] ! P ∣ P ∼ ! P
6-1-2 {P} =
⟨ (λ {P′} {μ} tr →
P′ ∼⟨ ∼′: reflexive ⟩■
P′ [ μ ]⟵⟨ replication tr ⟩
! P)
, (λ { {q′ = P′} {μ = μ} (replication tr) →
! P ∣ P [ μ ]⟶⟨ tr ⟩ʳˡ
P′ ∼⟨ ∼′: reflexive ⟩■
P′ })
⟩
private
module 6-1-3-2 = Bisimilarity.CCS.General.6-1-3-2 (record
{ _∼_ = _∼_
; step-∼ = step-∼
; finally-∼ = Equational-reasoning.finally₂
; reflexive = reflexive
; symmetric = symmetric
; ∣-comm = ∣-comm
; ∣-assoc = ∣-assoc
; _∣-cong_ = _∣-cong_
; 6-1-2 = 6-1-2
})
6-1-3-2 :
∀ {P μ R} →
! P [ μ ]⟶ R →
(∃ λ P′ → P [ μ ]⟶ P′ × R ∼ ! P ∣ P′)
⊎
(μ ≡ τ × ∃ λ P′ → ∃ λ P″ → ∃ λ a →
P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ × R ∼ (! P ∣ P′) ∣ P″)
6-1-3-2 = 6-1-3-2.6-1-3-2
swap-rightmost : ∀ {P Q R} → (P ∣ Q) ∣ R ∼ (P ∣ R) ∣ Q
swap-rightmost = 6-1-3-2.swap-rightmost
swap-in-the-middle : ∀ {P Q R S} →
(P ∣ Q) ∣ (R ∣ S) ∼ (P ∣ R) ∣ (Q ∣ S)
swap-in-the-middle {P} {Q} {R} {S} =
(P ∣ Q) ∣ (R ∣ S) ∼⟨ swap-rightmost ⟩
(P ∣ (R ∣ S)) ∣ Q ∼⟨ ∣-assoc ∣-cong reflexive ⟩
((P ∣ R) ∣ S) ∣ Q ∼⟨ symmetric ∣-assoc ⟩
(P ∣ R) ∣ (S ∣ Q) ∼⟨ reflexive ∣-cong ∣-comm ⟩■
(P ∣ R) ∣ (Q ∣ S)
infix 8 _⊕-cong_ _⊕-cong′_
_⊕-cong_ : ∀ {i P P′ Q Q′} →
[ i ] P ∼ P′ → [ i ] Q ∼ Q′ → [ i ] P ⊕ Q ∼ P′ ⊕ Q′
_⊕-cong_ {i} P∼P′ Q∼Q′ =
⟨ CL.⊕-cong P∼P′ Q∼Q′
, Σ-map id (Σ-map id symmetric) ∘
CL.⊕-cong {i = i} (symmetric P∼P′) (symmetric Q∼Q′)
⟩
_⊕-cong′_ : ∀ {i P P′ Q Q′} →
[ i ] P ∼′ P′ → [ i ] Q ∼′ Q′ → [ i ] P ⊕ Q ∼′ P′ ⊕ Q′
force (P∼P′ ⊕-cong′ Q∼Q′) = force P∼P′ ⊕-cong force Q∼Q′
infix 12 _·-cong_ _·-cong′_
_·-cong_ :
∀ {i μ μ′ P P′} →
μ ≡ μ′ → [ i ] force P ∼′ force P′ → [ i ] μ · P ∼ μ′ · P′
refl ·-cong P∼P′ =
⟨ CL.·-cong P∼P′
, Σ-map id (Σ-map id symmetric) ∘ CL.·-cong (symmetric P∼P′)
⟩
_·-cong′_ :
∀ {i μ μ′ P P′} →
μ ≡ μ′ → [ i ] force P ∼′ force P′ → [ i ] μ · P ∼′ μ′ · P′
force (μ≡μ′ ·-cong′ P∼P′) = μ≡μ′ ·-cong P∼P′
·-congP : ∀ {i μ P Q} → [ i ] force P ∼′ force Q → [ i ] μ · P ∼ μ · Q
·-congP p =
⟨ (λ { action → _ , action , p })
, (λ { action → _ , action , p })
⟩
infix 12 _∙-cong_ _∙-cong′_
_∙-cong_ :
∀ {i μ μ′ P P′} →
μ ≡ μ′ → [ i ] P ∼ P′ → [ i ] μ ∙ P ∼ μ′ ∙ P′
refl ∙-cong P∼P′ = refl ·-cong convert {a = ℓ} P∼P′
_∙-cong′_ :
∀ {i μ μ′ P P′} →
μ ≡ μ′ → [ i ] P ∼′ P′ → [ i ] μ ∙ P ∼′ μ′ ∙ P′
force (μ≡μ′ ∙-cong′ P∼P′) = μ≡μ′ ∙-cong force P∼P′
infix 12 _∙-cong _∙-cong′
_∙-cong : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ∼ μ′ ∙
refl ∙-cong = reflexive
_∙-cong′ : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ∼′ μ′ ∙
refl ∙-cong′ = reflexive
mutual
infix 10 !-cong_ !-cong′_
!-cong_ : ∀ {i P P′} →
[ i ] P ∼ P′ → [ i ] ! P ∼ ! P′
!-cong P∼P′ =
⟨ lr P∼P′
, Σ-map id (Σ-map id symmetric) ∘ lr (symmetric P∼P′)
⟩
where
lr = CL.!-cong 6-1-3-2 _∣-cong′_ !-cong′_
!-cong′_ : ∀ {i P P′} → [ i ] P ∼′ P′ → [ i ] ! P ∼′ ! P′
force (!-cong′ P∼P′) = !-cong force P∼P′
!-congP : ∀ {i P Q} → [ i ] P ∼ Q → [ i ] ! P ∼ ! Q
!-congP {i} = λ p →
⟨ lr p
, Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p)
⟩
where
lr : ∀ {P Q R μ} →
[ i ] P ∼ Q → ! P [ μ ]⟶ R →
∃ λ S → ! Q [ μ ]⟶ S × [ i ] R ∼′ S
lr {P} {Q} {R} P∼Q !P⟶R with 6-1-3-2 !P⟶R
... | inj₁ (P′ , P⟶P′ , R∼!P∣P′) =
let (Q′ , Q⟶Q′ , P′∼′Q′) = left-to-right P∼Q P⟶P′
in
( ! Q ∣ Q′
, replication (par-right Q⟶Q′)
, (R ∼⟨ R∼!P∣P′ ⟩
! P ∣ P′ ∼⟨ (λ { .force → !-congP P∼Q }) ∣-cong′ P′∼′Q′ ⟩
! Q ∣ Q′ ■
)
)
... | inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , R∼!P∣P′∣P″) =
let (Q′ , Q⟶Q′ , P′∼′Q′) = left-to-right P∼Q P⟶P′
(Q″ , Q⟶Q″ , P″∼′Q″) = left-to-right P∼Q P⟶P″
in
( (! Q ∣ Q′) ∣ Q″
, replication (par-τ (replication (par-right Q⟶Q′)) Q⟶Q″)
, (R ∼⟨ R∼!P∣P′∣P″ ⟩
(! P ∣ P′) ∣ P″ ∼⟨ ((λ { .force → !-congP P∼Q }) ∣-cong′ P′∼′Q′)
∣-cong′ P″∼′Q″ ⟩
(! Q ∣ Q′) ∣ Q″ ■
)
)
mutual
⟨ν_⟩-cong : ∀ {i a a′ P P′} →
a ≡ a′ → [ i ] P ∼ P′ → [ i ] ⟨ν a ⟩ P ∼ ⟨ν a′ ⟩ P′
⟨ν refl ⟩-cong = λ P∼P′ →
⟨ lr P∼P′
, Σ-map id (Σ-map id symmetric) ∘ lr (symmetric P∼P′)
⟩
where
lr = CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′
⟨ν_⟩-cong′ : ∀ {i a a′ P P′} →
a ≡ a′ → [ i ] P ∼′ P′ → [ i ] ⟨ν a ⟩ P ∼′ ⟨ν a′ ⟩ P′
force (⟨ν a≡a′ ⟩-cong′ P∼P′) = ⟨ν a≡a′ ⟩-cong (force P∼P′)
infix 5 _[_]-cong _[_]-cong′
_[_]-cong :
∀ {i n Ps Qs}
(C : Context ∞ n) → (∀ x → [ i ] Ps x ∼ Qs x) →
[ i ] C [ Ps ] ∼ C [ Qs ]
hole x [ Ps∼Qs ]-cong = Ps∼Qs x
∅ [ Ps∼Qs ]-cong = reflexive
C₁ ∣ C₂ [ Ps∼Qs ]-cong = (C₁ [ Ps∼Qs ]-cong) ∣-cong (C₂ [ Ps∼Qs ]-cong)
C₁ ⊕ C₂ [ Ps∼Qs ]-cong = (C₁ [ Ps∼Qs ]-cong) ⊕-cong (C₂ [ Ps∼Qs ]-cong)
μ · C [ Ps∼Qs ]-cong = refl ·-cong λ { .force → force C [ Ps∼Qs ]-cong }
⟨ν a ⟩ C [ Ps∼Qs ]-cong = ⟨ν refl ⟩-cong (C [ Ps∼Qs ]-cong)
! C [ Ps∼Qs ]-cong = !-cong (C [ Ps∼Qs ]-cong)
_[_]-cong′ :
∀ {i n Ps Qs}
(C : Context ∞ n) → (∀ x → [ i ] Ps x ∼′ Qs x) →
[ i ] C [ Ps ] ∼′ C [ Qs ]
force (C [ Ps∼Qs ]-cong′) = C [ (λ x → force (Ps∼Qs x)) ]-cong
module _ (ext : Proc-extensionality) where
mutual
infix 5 _[_]-cong₂ _[_]-cong₂′
_[_]-cong₂ :
∀ {i n Ps Qs}
(C : Context ∞ n) → (∀ x → [ i ] Ps x ∼ Qs x) →
[ i ] C [ Ps ] ∼ C [ Qs ]
_[_]-cong₂ {i} C Ps∼Qs =
⟨ lr C Ps∼Qs
, Σ-map id (Σ-map id symmetric) ∘ lr C (symmetric ∘ Ps∼Qs)
⟩
where
infix 5 _[_][_]-cong₁ _[_][_]-cong₂
_[_][_]-cong₁ :
∀ {n P Q Ps Qs} →
(C : Context ∞ (suc n)) →
[ i ] P ∼′ Q →
(∀ x → [ i ] Ps x ∼ Qs x) →
[ i ] C [ [ const P , Ps ] ] ∼′ C [ [ const Q , Qs ] ]
force (C [ P∼′Q ][ Ps∼Qs ]-cong₁) =
C [ [ const (force P∼′Q) , Ps∼Qs ] ]-cong₂
_[_][_]-cong₂ :
∀ {P Q R S} →
(C : Context ∞ 2) →
[ i ] P ∼′ Q →
[ i ] R ∼′ S →
[ i ] C [ [ const P , [ const R , (λ ()) ] ] ] ∼′
C [ [ const Q , [ const S , (λ ()) ] ] ]
force (C [ P∼′Q ][ R∼′S ]-cong₂) =
C [ [ const (force P∼′Q)
, [ const (force R∼′S) , (λ ()) ]
] ]-cong₂
lr : ∀ {n Ps Qs P′ μ} (C : Context ∞ n) →
(∀ x → [ i ] Ps x ∼ Qs x) →
C [ Ps ] [ μ ]⟶ P′ →
∃ λ Q′ → C [ Qs ] [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
lr (hole x) Ps∼Qs tr = left-to-right (Ps∼Qs x) tr
lr ∅ Ps∼Qs ()
lr (C₁ ∣ C₂) Ps∼Qs (par-left tr) = Σ-map (_∣ _) (Σ-map par-left (λ b → subst (λ P → [ i ] _ ∼′ _ ∣ P) (ext $ weaken-[] C₂) $
subst (λ P → [ i ] _ ∣ P ∼′ _) (ext $ weaken-[] C₂) $
hole fzero ∣ weaken C₂ [ b ][ Ps∼Qs ]-cong₁)) (lr C₁ Ps∼Qs tr)
lr (C₁ ∣ C₂) Ps∼Qs (par-right tr) = Σ-map (_ ∣_) (Σ-map par-right (λ b → subst (λ P → [ i ] _ ∼′ P ∣ _) (ext $ weaken-[] C₁) $
subst (λ P → [ i ] P ∣ _ ∼′ _) (ext $ weaken-[] C₁) $
weaken C₁ ∣ hole fzero [ b ][ Ps∼Qs ]-cong₁)) (lr C₂ Ps∼Qs tr)
lr (C₁ ∣ C₂) Ps∼Qs (par-τ tr₁ tr₂) = Σ-zip _∣_ (Σ-zip par-τ (λ b₁ b₂ → hole fzero ∣ hole (fsuc fzero) [ b₁ ][ b₂ ]-cong₂))
(lr C₁ Ps∼Qs tr₁) (lr C₂ Ps∼Qs tr₂)
lr (C₁ ⊕ C₂) Ps∼Qs (sum-left tr) = Σ-map id (Σ-map sum-left id) (lr C₁ Ps∼Qs tr)
lr (C₁ ⊕ C₂) Ps∼Qs (sum-right tr) = Σ-map id (Σ-map sum-right id) (lr C₂ Ps∼Qs tr)
lr (μ · C) Ps∼Qs action = _ , action , λ { .force → force C [ Ps∼Qs ]-cong₂ }
lr (⟨ν a ⟩ C) Ps∼Qs (restriction a∉ tr) = Σ-map ⟨ν a ⟩ (Σ-map (restriction a∉) (λ b → ⟨ν a ⟩ (hole fzero) [ b ][ Ps∼Qs ]-cong₁))
(lr C Ps∼Qs tr)
lr (! C) Ps∼Qs (replication tr) = Σ-map id (Σ-map replication id) (lr (! C ∣ C) Ps∼Qs tr)
_[_]-cong₂′ :
∀ {i n Ps Qs}
(C : Context ∞ n) → (∀ x → [ i ] Ps x ∼′ Qs x) →
[ i ] C [ Ps ] ∼′ C [ Qs ]
force (C [ Ps∼′Qs ]-cong₂′) = C [ (λ x → force (Ps∼′Qs x)) ]-cong₂
infix 5 _[_]-cong-w
_[_]-cong-w :
∀ {i n Ps Qs} {C : Context ∞ n} →
Weakly-guarded C → (∀ x → [ i ] Ps x ∼′ Qs x) →
[ i ] C [ Ps ] ∼ C [ Qs ]
∅ [ Ps∼Qs ]-cong-w = reflexive
W₁ ∣ W₂ [ Ps∼Qs ]-cong-w = (W₁ [ Ps∼Qs ]-cong-w) ∣-cong
(W₂ [ Ps∼Qs ]-cong-w)
action {C = C} [ Ps∼Qs ]-cong-w = refl ·-cong (force C [ Ps∼Qs ]-cong′)
⟨ν⟩ W [ Ps∼Qs ]-cong-w = ⟨ν refl ⟩-cong (W [ Ps∼Qs ]-cong-w)
! W [ Ps∼Qs ]-cong-w = !-cong (W [ Ps∼Qs ]-cong-w)
W₁ ⊕ W₂ [ Ps∼Qs ]-cong-w = (W₁ [ Ps∼Qs ]-cong-w) ⊕-cong
(W₂ [ Ps∼Qs ]-cong-w)
mutual
≡→∼ : ∀ {i P Q} → Equal i P Q → [ i ] P ∼ Q
≡→∼ ∅ = reflexive
≡→∼ (eq₁ ∣ eq₂) = ≡→∼ eq₁ ∣-cong ≡→∼ eq₂
≡→∼ (eq₁ ⊕ eq₂) = ≡→∼ eq₁ ⊕-cong ≡→∼ eq₂
≡→∼ (refl · eq) = refl ·-cong ≡→∼′ eq
≡→∼ (⟨ν refl ⟩ eq) = ⟨ν refl ⟩-cong (≡→∼ eq)
≡→∼ (! eq) = !-cong ≡→∼ eq
≡→∼′ : ∀ {i P Q} → Equal′ i P Q → [ i ] P ∼′ Q
force (≡→∼′ eq) = ≡→∼ (force eq)
mutual
unique-solutions :
∀ {i n} {Ps Qs : Fin n → Proc ∞} {C : Fin n → Context ∞ n} →
(∀ x → Weakly-guarded (C x)) →
(∀ x → [ i ] Ps x ∼ C x [ Ps ]) →
(∀ x → [ i ] Qs x ∼ C x [ Qs ]) →
∀ x → [ i ] Ps x ∼ Qs x
unique-solutions {i} {Ps = Ps} {Qs} {C} w ∼C[Ps] ∼C[Qs] x =
Ps x ∼⟨ ∼C[Ps] x ⟩
C x [ Ps ] ∼⟨ ∼: ⟨ lr ∼C[Ps] ∼C[Qs] , Σ-map id (Σ-map id symmetric) ∘ lr ∼C[Qs] ∼C[Ps] ⟩ ⟩
C x [ Qs ] ∼⟨ symmetric (∼C[Qs] x) ⟩■
Qs x
where
lr :
∀ {Ps Qs μ P} →
(∀ x → [ i ] Ps x ∼ C x [ Ps ]) →
(∀ x → [ i ] Qs x ∼ C x [ Qs ]) →
C x [ Ps ] [ μ ]⟶ P →
∃ λ Q → C x [ Qs ] [ μ ]⟶ Q × [ i ] P ∼′ Q
lr {Ps} {Qs} {μ} ∼C[Ps] ∼C[Qs] ⟶P =
case 6-2-15 (C x) (w x) ⟶P of λ where
(C′ , refl , trs) →
C′ [ Ps ] ∼⟨ C′ [ unique-solutions′ w ∼C[Ps] ∼C[Qs] ]-cong′ ⟩■
C′ [ Qs ] [ μ ]⟵⟨ trs Qs ⟩
C x [ Qs ]
unique-solutions′ :
∀ {i n} {Ps Qs : Fin n → Proc ∞} {C : Fin n → Context ∞ n} →
(∀ x → Weakly-guarded (C x)) →
(∀ x → [ i ] Ps x ∼ C x [ Ps ]) →
(∀ x → [ i ] Qs x ∼ C x [ Qs ]) →
∀ x → [ i ] Ps x ∼′ Qs x
force (unique-solutions′ w ∼C[Ps] ∼C[Qs] x) = unique-solutions w ∼C[Ps] ∼C[Qs] x
solutions-exist :
∀ {n} {C : Fin n → Context ∞ n} →
(∀ x → Weakly-guarded (C x)) →
∃ λ Ps → ∀ x → Ps x ∼ C x [ Ps ]
solutions-exist {n} {C} w = Ps , Ps∼
where
mutual
Ps : ∀ {i} → Fin n → Proc i
Ps x = P₁ (w x)
P₁ : ∀ {i} {C : Context ∞ n} → Weakly-guarded C → Proc i
P₁ ∅ = ∅
P₁ (w₁ ∣ w₂) = P₁ w₁ ∣ P₁ w₂
P₁ (w₁ ⊕ w₂) = P₁ w₁ ⊕ P₁ w₂
P₁ (action {μ = μ} {C = C}) = μ · λ { .force → P₂ (force C) }
P₁ (⟨ν⟩ {a = a} w) = ⟨ν a ⟩ (P₁ w)
P₁ (! w) = ! P₁ w
P₂ : ∀ {i} → Context ∞ n → Proc i
P₂ (hole x) = Ps x
P₂ ∅ = ∅
P₂ (C₁ ∣ C₂) = P₂ C₁ ∣ P₂ C₂
P₂ (C₁ ⊕ C₂) = P₂ C₁ ⊕ P₂ C₂
P₂ (μ · C) = μ · λ { .force → P₂ (force C) }
P₂ (⟨ν a ⟩ C) = ⟨ν a ⟩ (P₂ C)
P₂ (! C) = ! P₂ C
P₂∼ : ∀ {i} (C : Context ∞ n) → [ i ] P₂ C ∼ C [ Ps ]
P₂∼ (hole x) = reflexive
P₂∼ ∅ = reflexive
P₂∼ (C₁ ∣ C₂) = P₂∼ C₁ ∣-cong P₂∼ C₂
P₂∼ (C₁ ⊕ C₂) = P₂∼ C₁ ⊕-cong P₂∼ C₂
P₂∼ (μ · C) = refl ·-cong λ { .force → P₂∼ (force C) }
P₂∼ (⟨ν a ⟩ C) = ⟨ν refl ⟩-cong (P₂∼ C)
P₂∼ (! C) = !-cong P₂∼ C
P₁∼ : {C : Context ∞ n} (w : Weakly-guarded C) → P₁ w ∼ C [ Ps ]
P₁∼ ∅ = reflexive
P₁∼ (w₁ ∣ w₂) = P₁∼ w₁ ∣-cong P₁∼ w₂
P₁∼ (w₁ ⊕ w₂) = P₁∼ w₁ ⊕-cong P₁∼ w₂
P₁∼ (action {C = C}) = refl ·-cong λ { .force → P₂∼ (force C) }
P₁∼ (⟨ν⟩ {a = a} w) = ⟨ν refl ⟩-cong (P₁∼ w)
P₁∼ (! w) = !-cong P₁∼ w
Ps∼ : ∀ x → Ps x ∼ C x [ Ps ]
Ps∼ x = P₁∼ (w x)
⊕-idempotent : ∀ {P} → P ⊕ P ∼ P
⊕-idempotent {P} =
⟨ lr
, (λ {R} P⟶R →
P ⊕ P ⟶⟨ sum-left P⟶R ⟩ʳˡ
R ∼⟨ ∼′: reflexive ⟩■
R)
⟩
where
lr : ∀ {Q μ} → P ⊕ P [ μ ]⟶ Q → ∃ λ R → P [ μ ]⟶ R × Q ∼′ R
lr {Q} (sum-left P⟶Q) =
Q ∼⟨ ∼′: reflexive ⟩■
Q ⟵⟨ P⟶Q ⟩
P
lr {Q} (sum-right P⟶Q) =
Q ∼⟨ ∼′: reflexive ⟩■
Q ⟵⟨ P⟶Q ⟩
P
⊕-idempotent′ : ∀ {P} → P ⊕ P ∼′ P
force ⊕-idempotent′ = ⊕-idempotent
⊕-comm : ∀ {P Q} → P ⊕ Q ∼ Q ⊕ P
⊕-comm = ⟨ lr , Σ-map id (Σ-map id symmetric) ∘ lr ⟩
where
lr : ∀ {P Q R μ} →
P ⊕ Q [ μ ]⟶ R → ∃ λ R′ → Q ⊕ P [ μ ]⟶ R′ × R ∼′ R′
lr {P} {Q} {R} = λ where
(sum-left P⟶R) →
R ■ ⟵⟨ sum-right P⟶R ⟩
Q ⊕ P
(sum-right Q⟶R) →
R ■ ⟵⟨ sum-left Q⟶R ⟩
Q ⊕ P