{-# OPTIONS --no-termination-check --lossy-unification #-}
module CCS.Proc where
open import Prelude hiding (P; ℕ)
open import CCS.Alg
open import CCS.SemiModel
open import Data.Set renaming (⟦_⟧ to 𝒦⟦_⟧)
import Data.Set
record Proc (A : Type a) : Type a where
coinductive
constructor ⟪_⟫
field ↯ : 𝒦 (Act A × Proc A)
open Proc public
module ProcIso𝒦 where
opaque
Proc⇔𝒦 : Proc A ⇔ 𝒦 (Act A × Proc A)
Proc⇔𝒦 .fun = ↯
Proc⇔𝒦 .inv = ⟪_⟫
Proc⇔𝒦 .rightInv x = refl
Proc⇔𝒦 .leftInv x i .↯ = x .↯
opaque
isSetProc : isSet (Proc A)
isSetProc = subst isSet (sym (isoToPath Proc⇔𝒦)) trunc
open ProcIso𝒦 using (isSetProc) public
proc∘↯ : (xs : Proc A) → ⟪ ↯ xs ⟫ ≡ xs
proc∘↯ xs i .↯ = ↯ xs
cong-proc : {xs ys : Proc A} → ↯ xs ≡ ↯ ys → xs ≡ ys
cong-proc eq i .↯ = eq i
_guarding_ : Bool → 𝒦 A → 𝒦 A
_guarding_ = flip (bool ∅)
guarding->>= : ∀ b (xs : 𝒦 A) (k : A → 𝒦 B) → (b guarding xs) >>= k ≡ b guarding (xs >>= k)
guarding->>= false xs k = refl
guarding->>= true xs k = refl
module ProcAlg where
infixl 5 _⊕_
infixr 7 _·_
_·_ : Act A → Proc A → Proc A
a · p = ⟪ ⟅ a , p ⟆ ⟫
𝟘 : Proc A
𝟘 = ⟪ ∅ ⟫
_⊕_ : Proc A → Proc A → Proc A
p ⊕ q = ⟪ ↯ p ∪ ↯ q ⟫
⊕-assoc : (x y z : Proc A) → (x ⊕ y) ⊕ z ≡ x ⊕ (y ⊕ z)
⊕-assoc x y z = cong-proc (assoc _ _ _)
⊕-comm : (x y : Proc A) → x ⊕ y ≡ y ⊕ x
⊕-comm x y = cong-proc (comm _ _)
𝟘⊕ : (x : Proc A) → 𝟘 ⊕ x ≡ x
𝟘⊕ x = cong-proc (ident _)
⊕𝟘 : (x : Proc A) → x ⊕ 𝟘 ≡ x
⊕𝟘 x = ⊕-comm x 𝟘 ⨾ 𝟘⊕ x
⊕-idem : (x : Proc A) → x ⊕ x ≡ x
⊕-idem x = cong-proc (idem _)
ρ : (A → B) → Proc A → Proc B
ρ$ : (A → B) → Act A × Proc A → Act B × Proc B
ρ f x .↯ = ↯ x >>- ρ$ f
ρ$ f = map-Σ (map-act f) (ρ f)
steps stepsₗ : Proc A → Proc A → Proc A
stepsₗ p q .↯ = ↯ p >>- map₂ (steps q)
steps p q = stepsₗ p q ⊕ stepsₗ q p
module _ ⦃ _ : IsDiscrete A ⦄ where
infixl 6 _∥_ _⌊_
infixr 7 ν_-_
_∥_ : Proc A → Proc A → Proc A
_⌊_ : Proc A → Proc A → Proc A
_⌊ₖ_ : Act A × Proc A → Proc A → 𝒦 (Act A × Proc A)
syncₐₒ : Act A → Proc A → Proc A → 𝒦 (Act A × Proc A)
syncₒ : A → Proc A → Proc A → 𝒦 (Act A × Proc A)
syncₒₖ : A → Proc A → Act A × Proc A → 𝒦 (Act A × Proc A)
(p ∥ q) .↯ = ↯ (p ⌊ q) ∪ ↯ (q ⌊ p)
(p ⌊ q) .↯ = p .↯ >>= (_⌊ₖ q)
((a , p′) ⌊ₖ q) = syncₐₒ a p′ q ∪ ⟅ a , (p′ ∥ q) ⟆
syncₐₒ (inp a) p q = syncₒ a p q
syncₐₒ (out _) p q = ∅
syncₐₒ τ p q = ∅
syncₒ a p q = ↯ q >>= syncₒₖ a p
syncₒₖ a p (out b , q′) = does (a ≟ b) guarding ⟅ τ , (p ∥ q′) ⟆
syncₒₖ a p _ = ∅
open import Data.Bool.Properties
syncₒₖ>>=syncₒₖ : ∀ a p b r bq → (syncₒₖ a p bq >>= syncₒₖ b r) ≡ ∅
syncₒₖ>>=syncₒₖ a p b r (inp _ , q) = refl
syncₒₖ>>=syncₒₖ a p b r (τ , q) = refl
syncₒₖ>>=syncₒₖ a p b r (out c , q) = guarding->>= (does (a ≟ c)) _ _ ⨾ if-idem _ _
stepₗ : Proc A → Proc A → Proc A
stepₗ p q .↯ = 𝒦-map (map₂ (_∥ q)) (↯ p)
syncᵢₒ : Proc A → Proc A → Proc A
syncᵢₒ p q .↯ = do
a , p′ ← ↯ p
syncₐₒ a p′ q
step-sync : ∀ p q → p ⌊ q ≡ syncᵢₒ p q ⊕ stepₗ p q
step-sync p q = cong-proc (>>=-∪ (↯ p) (flip (uncurry syncₐₒ) q) (⟅_⟆ ∘ map₂ (_∥ q)))
step-is-step : ∀ a p q → stepₗ (a · p) q ≡ a · (p ∥ q)
step-is-step a p q = cong-proc refl
syncₒ∘syncₒ : ∀ a b p q r → syncₒ a p ⟪ syncₒ b q r ⟫ ≡ ∅
syncₒ∘syncₒ a b p q r =
syncₒ a p ⟪ syncₒ b q r ⟫ ≡⟨⟩
(r .↯ >>= syncₒₖ b q) >>= syncₒₖ a p ≡⟨ >>=-assoc (r .↯) _ _ ⟩
r .↯ >>= (λ r′ → syncₒₖ b q r′ >>= syncₒₖ a p) ≡⟨ cong (r .↯ >>=_) (funExt (syncₒₖ>>=syncₒₖ b q a p)) ⟩
r .↯ >>= const ∅ ≡⟨ >>=∅ (r .↯) ⟩
∅ ∎
syncₒₖ>>=syncₐₒ : ∀ a p r q′ → syncₒₖ a p q′ >>= flip (uncurry syncₐₒ) r ≡ ∅
syncₒₖ>>=syncₐₒ a p r (inp x₁ , q′) = refl
syncₒₖ>>=syncₐₒ a p r (τ , q′) = refl
syncₒₖ>>=syncₐₒ a p r (out b , q′) = guarding->>= (does (a ≟ b)) _ _ ⨾ if-idem ∅ (does (a ≟ b))
syncₐₒ>>=syncₐₒ : ∀ q r p′ → uncurry syncₐₒ p′ q >>= flip (uncurry syncₐₒ) r ≡ ∅
syncₐₒ>>=syncₐₒ q r (τ , p′) = refl
syncₐₒ>>=syncₐₒ q r (out x₁ , p′) = refl
syncₐₒ>>=syncₐₒ q r (inp a , p′) =
syncₒ a p′ q >>= flip (uncurry syncₐₒ) r ≡⟨⟩
(↯ q >>= syncₒₖ a p′) >>= flip (uncurry syncₐₒ) r ≡⟨ >>=-assoc _ _ _ ⟩
↯ q >>= (λ q′ → syncₒₖ a p′ q′ >>= flip (uncurry syncₐₒ) r) ≡⟨ cong (↯ q >>=_) (funExt (syncₒₖ>>=syncₐₒ _ _ _)) ⟩
↯ q >>= const ∅ ≡⟨ >>=∅ (↯ q) ⟩
∅ ∎
syncᵢₒ∘syncᵢₒˡ : ∀ p q r → syncᵢₒ (syncᵢₒ p q) r ≡ 𝟘
syncᵢₒ∘syncᵢₒˡ p q r =
syncᵢₒ (syncᵢₒ p q) r ≡⟨ cong (flip syncᵢₒ r) (cong-proc refl) ⟩
syncᵢₒ ⟪ ↯ p >>= flip (uncurry syncₐₒ) q ⟫ r ≡⟨ cong-proc refl ⟩
⟪ (↯ p >>= flip (uncurry syncₐₒ) q) >>= flip (uncurry syncₐₒ) r ⟫ ≡⟨ cong ⟪_⟫ (>>=-assoc _ _ _) ⟩
⟪ ↯ p >>= (λ p′ → flip (uncurry syncₐₒ) q p′ >>= flip (uncurry syncₐₒ) r) ⟫ ≡⟨ cong (λ k → ⟪ ↯ p >>= k ⟫) (funExt (syncₐₒ>>=syncₐₒ q r)) ⟩
⟪ ↯ p >>= const ∅ ⟫ ≡⟨ cong-proc (>>=∅ (↯ p)) ⟩
𝟘 ∎
syncₐₒ>>=syncₒₖ : ∀ a p q b r → syncₐₒ a p q >>= syncₒₖ b r ≡ ∅
syncₐₒ>>=syncₒₖ (out _) p q b r = refl
syncₐₒ>>=syncₒₖ τ p q b r = refl
syncₐₒ>>=syncₒₖ (inp a) p q b r =
syncₒ a p q >>= syncₒₖ b r ≡⟨⟩
(↯ q >>= syncₒₖ a p) >>= syncₒₖ b r ≡⟨ >>=-assoc (↯ q) _ _ ⟩
↯ q >>= (λ q′ → syncₒₖ a p q′ >>= syncₒₖ b r) ≡⟨ cong (↯ q >>=_) (funExt (syncₒₖ>>=syncₒₖ a p b r) ) ⟩
↯ q >>= const ∅ ≡⟨ >>=∅ (↯ q) ⟩
∅ ∎
syncᵢₒ∘syncᵢₒ : ∀ p q r → syncᵢₒ p (syncᵢₒ q r) ≡ 𝟘
syncᵢₒ∘syncᵢₒ p q r =
syncᵢₒ p (syncᵢₒ q r) ≡⟨ cong-proc refl ⟩
⟪ p .↯ >>= flip (uncurry syncₐₒ) (syncᵢₒ q r) ⟫ ≡⟨ cong-proc (cong (p .↯ >>=_) (funExt (uncurry (lemma q r)))) ⟩
⟪ p .↯ >>= const ∅ ⟫ ≡⟨ cong-proc (>>=∅ (p .↯)) ⟩
𝟘 ∎
where
lemma : ∀ q r a p → syncₐₒ a p (syncᵢₒ q r) ≡ ∅
lemma q r (out _) p = refl
lemma q r τ p = refl
lemma q r (inp a) p =
syncₒ a p (syncᵢₒ q r) ≡⟨⟩
syncᵢₒ q r .↯ >>= syncₒₖ a p ≡⟨⟩
(q .↯ >>= flip (uncurry syncₐₒ) r) >>= syncₒₖ a p ≡⟨ >>=-assoc (q .↯) _ _ ⟩
q .↯ >>= (λ q′ → uncurry syncₐₒ q′ r >>= syncₒₖ a p) ≡⟨ cong (q .↯ >>=_) (funExt (λ { (b , q′) → syncₐₒ>>=syncₒₖ b q′ r a p })) ⟩
q .↯ >>= const ∅ ≡⟨ >>=∅ (q .↯) ⟩
∅ ∎
ν_-_ : A → Proc A → Proc A
ν′ : A → Act A × Proc A → Maybe (Act A × Proc A)
(ν a - p) .↯ = 𝒦-cat-maybes (ν′ a) (↯ p)
ν′ a (b , p) = if does (a ∈ₐ? b) then nothing else just (b , ν a - p)
ν-∈-· : ∀ n a p → n ∈ₐ a → ν n - a · p ≡ 𝟘
ν-∈-· n a p n∈ₐa = cong-proc $ cong ⟅?⟆ (cong (bool _ _) (it-does (n ∈ₐ? a) n∈ₐa))
ν-∉-· : ∀ n a p → n ∉ₐ a → ν n - a · p ≡ a · ν n - p
ν-∉-· n a p n∉ₐa = cong-proc $ cong ⟅?⟆ (cong (bool _ _) (it-doesn't (n ∈ₐ? a) n∉ₐa))
! : Proc A → Proc A
! p .↯ = stepₗ (p ⊕ syncᵢₒ p p) (! p) .↯
∥-comm : ∀ p q → p ∥ q ≡ q ∥ p
∥-comm p q = cong-proc (comm _ _)
mutual
par𝟘 : ∀ p → stepₗ 𝟘 p ≡ 𝟘
par𝟘 p = cong-proc refl
par𝟘ʳ : ∀ p → stepₗ p 𝟘 ≡ p
par𝟘ʳ p = cong-proc (cong (flip 𝒦-map (↯ p)) (funExt λ x → cong (fst x ,_) (∥-comm (x .snd) 𝟘 ⨾ 𝟘∥ (x .snd))) ⨾ >>=-id (↯ p))
sync𝟘 : ∀ p → syncᵢₒ 𝟘 p ≡ 𝟘
sync𝟘 p = cong-proc refl
sync𝟘ʳ : ∀ p → syncᵢₒ p 𝟘 ≡ 𝟘
sync𝟘ʳ p =
syncᵢₒ p 𝟘 ≡⟨ cong-proc (cong (↯ p >>=_) (funExt λ { (inp x , p′) → refl ; (out x , p′) → refl ; (τ , p′) → refl })) ⟩
⟪ ↯ p >>= const ∅ ⟫ ≡⟨ cong-proc (>>=∅ (↯ p)) ⟩
𝟘 ∎
𝟘⌊ : ∀ p → 𝟘 ⌊ p ≡ 𝟘
𝟘⌊ p = cong-proc refl
⌊ₖ𝟘 : (ap : Act A × Proc A) → ap ⌊ₖ 𝟘 ≡ ⟅ ap ⟆
⌊ₖ𝟘 (out a , p′) = ident ⟅ out a , p′ ∥ 𝟘 ⟆ ⨾ cong (λ e → ⟅ out a , e ⟆) (∥𝟘 p′)
⌊ₖ𝟘 (τ , p′) = ident ⟅ τ , p′ ∥ 𝟘 ⟆ ⨾ cong (λ e → ⟅ τ , e ⟆) (∥𝟘 p′)
⌊ₖ𝟘 (inp a , p′) = ident ⟅ inp a , p′ ∥ 𝟘 ⟆ ⨾ cong (λ e → ⟅ inp a , e ⟆) (∥𝟘 p′)
⌊𝟘 : ∀ p → p ⌊ 𝟘 ≡ p
⌊𝟘 p = cong-proc (cong (p .↯ >>=_) (funExt ⌊ₖ𝟘) ⨾ >>=-id (p .↯))
𝟘∥ : ∀ p → 𝟘 ∥ p ≡ p
𝟘∥ p =
𝟘 ∥ p ≡⟨ cong-proc refl ⟩
𝟘 ⌊ p ⊕ p ⌊ 𝟘 ≡⟨ cong (_⊕ p ⌊ 𝟘) (𝟘⌊ p) ⟩
𝟘 ⊕ p ⌊ 𝟘 ≡⟨ cong-proc (ident _) ⟩
p ⌊ 𝟘 ≡⟨ ⌊𝟘 p ⟩
p ∎
∥𝟘 : ∀ p → p ∥ 𝟘 ≡ p
∥𝟘 p = ∥-comm p 𝟘 ⨾ 𝟘∥ p
opaque
⌊-∥ : ∀ p q → p ∥ q ≡ (p ⌊ q) ⊕ (q ⌊ p)
⌊-∥ p q = cong-proc refl
stepₗ-⊕ : ∀ x y z → stepₗ (x ⊕ y) z ≡ stepₗ x z ⊕ stepₗ y z
stepₗ-⊕ x y z = cong-proc (∪->>= _ (↯ x) (↯ y))
syncᵢₒ-⊕ : ∀ x y z → syncᵢₒ (x ⊕ y) z ≡ syncᵢₒ x z ⊕ syncᵢₒ y z
syncᵢₒ-⊕ x y z = cong-proc (∪->>= _ (↯ x) (↯ y))
opaque
syncᵢₒ-⊕ʳ : ∀ x y z → syncᵢₒ x (y ⊕ z) ≡ syncᵢₒ x y ⊕ syncᵢₒ x z
syncᵢₒ-⊕ʳ x y z = cong-proc (cong (↯ x >>=_) (funExt λ { (inp x , p) → refl ; (out x , p) → sym (ident _) ; (τ , p) → sym (ident _) }) ⨾ >>=-∪ (↯ x) _ _)
⊕⌊ : ∀ x y z → (x ⊕ y) ⌊ z ≡ (x ⌊ z) ⊕ (y ⌊ z)
⊕⌊ x y z = cong-proc refl
∥-assoc : ∀ x y z → (x ∥ y) ∥ z ≡ x ∥ (y ∥ z)
⌊-assoc : ∀ x y z → (x ⌊ y) ⌊ z ≡ x ⌊ (y ∥ z)
⌊²-comm : ∀ x y z → x ⌊ y ⌊ z ≡ x ⌊ z ⌊ y
syncᵢₒ-assoc : ∀ a p q r → syncᵢₒ (a · (p ∥ q)) r ≡ syncᵢₒ (a · p) (r ⌊ q)
⌊²-comm x y z =
x ⌊ y ⌊ z ≡⟨ ⌊-assoc x y z ⟩
x ⌊ (y ∥ z) ≡⟨ cong (x ⌊_) (∥-comm y z) ⟩
x ⌊ (z ∥ y) ≡˘⟨ ⌊-assoc x z y ⟩
x ⌊ z ⌊ y ∎
syncᵢₒ-assoc-⌊ : ∀ a p q r → syncᵢₒ (a · p) (q ⌊ r) ≡ syncᵢₒ (a · p) q ⌊ r
syncᵢₒ-assoc-⌊ τ p q r = cong-proc refl
syncᵢₒ-assoc-⌊ (out a) p q r = cong-proc refl
syncᵢₒ-assoc-⌊ (inp a) p q r = cong-proc $
↯ (syncᵢₒ (inp a · p) (q ⌊ r)) ≡⟨⟩
syncₒ a p (q ⌊ r) ≡⟨⟩
↯ (q ⌊ r) >>= syncₒₖ a p ≡⟨⟩
(↯ q >>= (_⌊ₖ r)) >>= syncₒₖ a p ≡⟨ >>=-assoc _ _ _ ⟩
↯ q >>= (λ q′ → (q′ ⌊ₖ r) >>= syncₒₖ a p) ≡⟨ cong (↯ q >>=_) (funExt (lemma₁ a p r)) ⟩
↯ q >>= (𝒦-map (map₂ (_∥ r)) ∘ syncₒₖ a p) ≡˘⟨ >>=-assoc _ _ _ ⟩
𝒦-map (map₂ (_∥ r)) (↯ q >>= syncₒₖ a p) ≡⟨⟩
𝒦-map (map₂ (_∥ r)) (syncₒ a p q) ≡⟨⟩
↯ (stepₗ ⟪ syncₒ a p q ⟫ r) ≡⟨⟩
↯ (stepₗ (syncᵢₒ (inp a · p) q) r) ≡˘⟨ cong ↯ (𝟘⊕ (((stepₗ (syncᵢₒ (inp a · p) q) r)))) ⟩
↯ (𝟘 ⊕ stepₗ (syncᵢₒ (inp a · p) q) r) ≡˘⟨ cong (λ e → ↯ (e ⊕ stepₗ (syncᵢₒ (inp a · p) q) r)) (syncᵢₒ∘syncᵢₒˡ _ _ _) ⟩
↯ (syncᵢₒ (syncᵢₒ (inp a · p) q) r ⊕ stepₗ (syncᵢₒ (inp a · p) q) r) ≡˘⟨ cong ↯ (step-sync (syncᵢₒ (inp a · p) q) r) ⟩
↯ (syncᵢₒ (inp a · p) q ⌊ r) ∎
where
lemma₂ : ∀ a p b q r → syncₒₖ a p (b , (q ∥ r)) ≡ 𝒦-map (map₂ (_∥ r)) (syncₒₖ a p (b , q))
lemma₂ a p τ q r = refl
lemma₂ a p (inp _) q r = refl
lemma₂ a p (out b) q r = cong (does (a ≟ b) guarding_) (cong (⟅_⟆ ∘ (_,_ τ)) (sym (∥-assoc p q r))) ⨾ sym (guarding->>= (does (a ≟ b)) ⟅ τ , p ∥ q ⟆ _)
lemma₁ : ∀ a p r q → (q ⌊ₖ r) >>= syncₒₖ a p ≡ 𝒦-map (map₂ (_∥ r)) (syncₒₖ a p q)
lemma₁ a p r (b , q ) =
((b , q) ⌊ₖ r) >>= syncₒₖ a p ≡⟨⟩
(syncₐₒ b q r ∪ ⟅ b , (q ∥ r) ⟆) >>= syncₒₖ a p ≡⟨⟩
(syncₐₒ b q r >>= syncₒₖ a p) ∪ syncₒₖ a p (b , (q ∥ r)) ≡⟨ cong (_∪ syncₒₖ a p (b , (q ∥ r))) (syncₐₒ>>=syncₒₖ b q r a p) ⟩
∅ ∪ syncₒₖ a p (b , (q ∥ r)) ≡⟨ ident _ ⟩
syncₒₖ a p (b , (q ∥ r)) ≡⟨ lemma₂ a p b q r ⟩
𝒦-map (map₂ (_∥ r)) (syncₒₖ a p (b , q)) ∎
⌊ₖ-assoc : ∀ (ap : Act A × Proc A) y z → ap ⌊ₖ y >>= (_⌊ₖ z) ≡ ap ⌊ₖ (y ∥ z)
⌊ₖ-assoc (a , p) y z = sym (assoc _ _ _) ⨾ cong₂ _∪_ (cong ↯ (lemma a p y z)) (cong (⟅_⟆ ∘ (_,_ a)) (∥-assoc p y z))
where
lemma : ∀ a p y z → (syncᵢₒ (a · p) y ⌊ z) ⊕ syncᵢₒ (a · (p ∥ y)) z ≡ syncᵢₒ (a · p) (y ∥ z)
lemma (out a) p y z = 𝟘⊕ _
lemma τ p y z = 𝟘⊕ _
lemma (inp a) p y z =
syncᵢₒ (inp a · p) y ⌊ z ⊕ syncᵢₒ (inp a · (p ∥ y)) z
≡⟨ cong₂ _⊕_ (sym (syncᵢₒ-assoc-⌊ (inp a) p y z)) (syncᵢₒ-assoc (inp a) p y z) ⟩
syncᵢₒ (inp a · p) (y ⌊ z) ⊕ syncᵢₒ (inp a · p) (z ⌊ y)
≡˘⟨ syncᵢₒ-⊕ʳ _ _ _ ⟩
syncᵢₒ (inp a · p) (y ⌊ z ⊕ z ⌊ y)
≡˘⟨ cong (syncᵢₒ (inp a · p)) (⌊-∥ y z) ⟩
syncᵢₒ (inp a · p) (y ∥ z) ∎
∥-assoc x y z =
(x ∥ y) ∥ z ≡⟨ ⌊-∥ (x ∥ y) z ⟩
(x ∥ y) ⌊ z ⊕ z ⌊ (x ∥ y) ≡˘⟨ cong₂ _⊕_ (cong (_⌊ z) (⌊-∥ _ _)) (⌊-assoc z x y) ⟩
(x ⌊ y ⊕ y ⌊ x) ⌊ z ⊕ (z ⌊ x ⌊ y) ≡⟨ cong (_⊕ (z ⌊ x ⌊ y)) (⊕⌊ _ _ _) ⟩
(x ⌊ y ⌊ z) ⊕ (y ⌊ x ⌊ z) ⊕ (z ⌊ x ⌊ y) ≡⟨ ⊕-assoc (x ⌊ y ⌊ z) (y ⌊ x ⌊ z) (z ⌊ x ⌊ y) ⟩
(x ⌊ y ⌊ z) ⊕ ((y ⌊ x ⌊ z) ⊕ (z ⌊ x ⌊ y)) ≡⟨ cong ((x ⌊ y ⌊ z) ⊕_) (cong₂ _⊕_ (⌊²-comm y x z) (⌊²-comm z x y)) ⟩
(x ⌊ y ⌊ z) ⊕ ((y ⌊ z ⌊ x) ⊕ (z ⌊ y ⌊ x)) ≡˘⟨ cong ((x ⌊ y ⌊ z) ⊕_) (⊕⌊ _ _ _) ⟩
(x ⌊ y ⌊ z) ⊕ (y ⌊ z ⊕ z ⌊ y) ⌊ x ≡⟨ cong₂ _⊕_ (⌊-assoc x y z) (cong (_⌊ x) (⌊-∥ y z)) ⟩
x ⌊ (y ∥ z) ⊕ (y ∥ z) ⌊ x ≡˘⟨ ⌊-∥ x (y ∥ z) ⟩
x ∥ (y ∥ z) ∎
⌊-assoc x y z = cong-proc $
↯ (x ⌊ y ⌊ z) ≡⟨⟩
↯ x >>= (_⌊ₖ y) >>= (_⌊ₖ z) ≡⟨ >>=-assoc (↯ x) _ _ ⟩
↯ x >>= (λ x′ → (x′ ⌊ₖ y) >>= (_⌊ₖ z)) ≡⟨ cong (↯ x >>=_) (funExt (λ ap → ⌊ₖ-assoc ap y z)) ⟩
↯ x >>= (_⌊ₖ (y ∥ z)) ≡⟨⟩
↯ (x ⌊ (y ∥ z)) ∎
syncᵢₒ-assoc τ p q r = cong-proc refl
syncᵢₒ-assoc (out _) p q r = cong-proc refl
syncᵢₒ-assoc (inp a) p q r = cong (λ e → syncᵢₒ (inp a · e) r) (∥-comm p q) ⨾ cong-proc (cong (r .↯ >>=_) (funExt (slemma a q p)) ⨾ sym (>>=-assoc (r .↯) (_⌊ₖ q) (syncₒₖ a p)))
where
slemma : ∀ a q r ps → syncₒₖ a (q ∥ r) ps ≡ ((ps ⌊ₖ q) >>= syncₒₖ a r)
slemma a q r (inp b , p′) =
∅ ≡˘⟨ syncₒ∘syncₒ a b r p′ q ⟩
syncₒ a r ⟪ syncₒ b p′ q ⟫ ≡˘⟨ ident _ ⟩
∅ ∪ (syncₒ b p′ q >>= syncₒₖ a r) ≡⟨⟩
( ⟅ inp b , p′ ∥ q ⟆ ∪ syncₒ b p′ q ) >>= syncₒₖ a r ≡⟨ cong (_>>= syncₒₖ a r) (comm _ _)⟩
( syncₒ b p′ q ∪ ⟅ inp b , p′ ∥ q ⟆ ) >>= syncₒₖ a r ≡⟨⟩
( (inp b , p′) ⌊ₖ q) >>= syncₒₖ a r ∎
slemma a q r (τ , p′) = sym (ident _)
slemma a q r (out b , p′) =
does (a ≟ b) guarding ⟅ τ , q ∥ r ∥ p′ ⟆ ≡⟨ cong (λ e → does (a ≟ b) guarding ⟅ τ , e ⟆) (cong (_∥ p′) (∥-comm q r) ⨾ ∥-assoc r q p′ ⨾ cong (r ∥_) (∥-comm q p′)) ⟩
does (a ≟ b) guarding ⟅ τ , r ∥ (p′ ∥ q) ⟆ ≡⟨⟩
syncₒₖ a r (out b , p′ ∥ q) ≡˘⟨ ident _ ⟩
∅ ∪ syncₒₖ a r (out b , p′ ∥ q) ≡⟨⟩
(((out b , p′) ⌊ₖ q) >>= syncₒₖ a r) ∎
syncᵢₒ-match : ∀ a b p q → a ∣ₗ b → syncᵢₒ (a · p) (b · q) ≡ τ · (p ∥ q)
syncᵢₒ-match (inp _) τ p q ()
syncᵢₒ-match (out _) τ p q ()
syncᵢₒ-match (inp a) (out b) p q a∣b = cong-proc (cong (bool _ _) (it-does (a ≟ b) a∣b))
syncᵢₒ-nomatch : ∀ a b p q → a ∤ₗ b → syncᵢₒ (a · p) (b · q) ≡ 𝟘
syncᵢₒ-nomatch τ b p q a∤b = cong-proc refl
syncᵢₒ-nomatch (out _) b p q a∤b = cong-proc refl
syncᵢₒ-nomatch (inp a) τ p q a∤b = cong-proc refl
syncᵢₒ-nomatch (inp a) (inp _) p q a∤b = cong-proc refl
syncᵢₒ-nomatch (inp a) (out b) p q a∤b = cong-proc (cong (bool _ _) (it-doesn't (a ≟ b) a∤b))
ν𝟘 : ∀ x → ν x - 𝟘 ≡ 𝟘
ν𝟘 x = cong-proc refl
ν-comm : ∀ x y p → ν x - ν y - p ≡ ν y - ν x - p
ν-comm x y p = cong-proc $
↯ (ν x - ν y - p) ≡⟨⟩
𝒦-cat-maybes (ν′ x) (𝒦-cat-maybes (ν′ y) (↯ p)) ≡⟨⟩
(↯ p >>= (⟅?⟆ ∘ (ν′ y))) >>= (⟅?⟆ ∘ (ν′ x)) ≡⟨ >>=-assoc (↯ p) _ _ ⟩
↯ p >>= (λ p′ → ⟅?⟆ (ν′ y p′) >>= (⟅?⟆ ∘ (ν′ x))) ≡⟨ cong (↯ p >>=_) (funExt lemma) ⟩
↯ p >>= (λ p′ → ⟅?⟆ (ν′ x p′) >>= (⟅?⟆ ∘ (ν′ y))) ≡˘⟨ >>=-assoc (↯ p) _ _ ⟩
𝒦-cat-maybes (ν′ y) (𝒦-cat-maybes (ν′ x) (↯ p)) ≡⟨⟩
↯ (ν y - ν x - p) ∎
where
lemma : ∀ p → ⟅?⟆ (ν′ y p) >>= (⟅?⟆ ∘ (ν′ x)) ≡ ⟅?⟆ (ν′ x p) >>= (⟅?⟆ ∘ (ν′ y))
lemma (a , p′) with x ∈ₐ? a | y ∈ₐ? a
... | yes x∈a | yes y∈a = refl
... | no x∉a | yes y∈a = sym (cong (maybe′ ∅ ⟅_⟆ ∘ bool′ _ 𝕥) (it-does (y ∈ₐ? a) y∈a))
... | yes x∈a | no y∉a = cong (maybe′ ∅ ⟅_⟆ ∘ bool′ _ 𝕥) (it-does (x ∈ₐ? a) x∈a)
... | no x∉a | no y∉a =
cong (maybe′ ∅ ⟅_⟆ ∘ bool′ _ _) (it-doesn't (x ∈ₐ? a) x∉a)
⨾ cong (⟅_⟆ ∘ (a ,_)) (ν-comm x y p′)
⨾ sym (cong (maybe′ ∅ ⟅_⟆ ∘ bool′ _ _) (it-doesn't (y ∈ₐ? a) y∉a))
ν-⊕ : ∀ x p q → ν x - (p ⊕ q) ≡ ν x - p ⊕ ν x - q
ν-⊕ x p q = cong-proc refl
stepₗ-assoc : ∀ p q r → stepₗ (stepₗ p q) r ≡ stepₗ p (q ∥ r)
stepₗ-assoc p q r =
stepₗ (stepₗ p q) r ≡⟨ cong-proc refl ⟩
⟪ ↯ (stepₗ p q) >>- map₂ (_∥ r) ⟫ ≡⟨⟩
⟪ (↯ p >>- map₂ (_∥ q)) >>- map₂ (_∥ r) ⟫ ≡⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ ↯ p >>= (λ { (a , p′) → ⟅ (a , (p′ ∥ q) ∥ r) ⟆ }) ⟫ ≡⟨ cong-proc (cong (↯ p >>=_) (funExt λ { (a , p′) → cong (⟅_⟆ ∘ (_,_ a)) (∥-assoc p′ q r) })) ⟩
⟪ ↯ p >>= (λ { (a , p′) → ⟅ a , p′ ∥ (q ∥ r) ⟆ }) ⟫ ≡⟨ cong-proc refl ⟩
stepₗ p (q ∥ r) ∎
sync-step-assoc : ∀ p q r → syncᵢₒ (stepₗ p q) r ≡ stepₗ (syncᵢₒ p r) q
sync-step-assoc p q r =
syncᵢₒ (stepₗ p q) r ≡⟨ cong-proc refl ⟩
⟪ ↯ (stepₗ p q) >>= (λ { (a , p′) → syncₐₒ a p′ r })⟫ ≡⟨⟩
⟪ (↯ p >>= λ { (a , p′) → ⟅ a , p′ ∥ q ⟆ }) >>= (λ { (b , q′) → syncₐₒ b q′ r })⟫ ≡⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ (↯ p >>= λ { (a , p′) → syncₐₒ a (p′ ∥ q) r }) ⟫ ≡⟨ cong-proc (cong (↯ p >>=_) (funExt (uncurry (lemma₁ q r)))) ⟩
⟪ ↯ p >>= (λ { (a , p′) → syncₐₒ a p′ r >>= (λ { (b , q′) → ⟅ (b , q′ ∥ q) ⟆ })}) ⟫ ≡˘⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ (↯ p >>= (λ { (a , p′) → syncₐₒ a p′ r })) >>= (λ { (b , q′) → ⟅ (b , q′ ∥ q) ⟆ }) ⟫ ≡⟨ cong-proc refl ⟩
⟪ ↯ (syncᵢₒ p r) >>= (λ { (a , p′) → ⟅ (a , p′ ∥ q) ⟆ }) ⟫ ≡⟨ cong-proc refl ⟩
stepₗ (syncᵢₒ p r) q ∎
where
lemma₂ : ∀ a p′ q r′ → syncₒₖ a (p′ ∥ q) r′ ≡ syncₒₖ a p′ r′ >>- map₂ (_∥ q)
lemma₂ a p′ q (inp x₁ , r′) = refl
lemma₂ a p′ q (τ , r′) = refl
lemma₂ a p′ q (out b , r′) = cong (flip (bool ∅) (does (a ≟ b))) (cong (⟅_⟆ ∘ (τ ,_)) (∥-assoc p′ q r′ ⨾ cong (p′ ∥_) (∥-comm q r′) ⨾ sym (∥-assoc p′ r′ q))) ⨾ sym (guarding->>= (does (a ≟ b)) _ _)
lemma₁ : ∀ q r a p′ → syncₐₒ a (p′ ∥ q) r ≡ syncₐₒ a p′ r >>- map₂ (_∥ q)
lemma₁ q r (out _) p′ = refl
lemma₁ q r τ p′ = refl
lemma₁ q r (inp a) p′ =
syncₒ a (p′ ∥ q) r ≡⟨⟩
↯ r >>= syncₒₖ a (p′ ∥ q) ≡⟨ cong (↯ r >>=_) (funExt (lemma₂ a p′ q)) ⟩
↯ r >>= (λ r′ → syncₒₖ a p′ r′ >>- map₂ (_∥ q)) ≡˘⟨ >>=-assoc _ _ _ ⟩
(↯ r >>= syncₒₖ a p′) >>- map₂ (_∥ q) ≡⟨⟩
syncₒ a p′ r >>- map₂ (_∥ q) ∎
step-sync-assoc : ∀ p q r → stepₗ (syncᵢₒ p q) r ≡ syncᵢₒ p (stepₗ q r)
step-sync-assoc p q r =
stepₗ (syncᵢₒ p q) r ≡⟨ cong-proc refl ⟩
⟪ (p .↯ >>= λ { (a , p′) → syncₐₒ a p′ q }) >>= (return ∘ map₂ (_∥ r)) ⟫ ≡⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ (p .↯ >>= λ { (a , p′) → syncₐₒ a p′ q >>= (return ∘ map₂ (_∥ r)) }) ⟫ ≡⟨ cong (λ e → ⟪ p .↯ >>= e ⟫) (funExt (uncurry (lemma q r))) ⟩
⟪ (p .↯ >>= λ { (a , p′) → syncₐₒ a p′ (stepₗ q r) }) ⟫ ≡⟨ cong-proc refl ⟩
syncᵢₒ p (stepₗ q r) ∎
where
lemma₃ : ∀ a p r b q → (d : Dec (a ≡ b)) → (syncₒₖ a p (out b , q) >>= return ∘ map₂ (_∥ r)) ≡ syncₒₖ a p (out b , q ∥ r)
lemma₃ a p r b q (no a≢b) = cong (_>>= _) (cong (bool′ _ _) (it-doesn't (a ≟ b) a≢b)) ⨾ sym (cong (bool′ _ _) (it-doesn't (a ≟ b) a≢b))
lemma₃ a p r b q (yes a≡b) = cong (_>>= _) (cong (bool′ _ _) (it-does (a ≟ b) a≡b)) ⨾ cong (⟅_⟆ ∘ (_,_ τ)) (∥-assoc p q r) ⨾ sym (cong (bool′ _ _) (it-does (a ≟ b) a≡b))
lemma₂ : ∀ a p r b q → (syncₒₖ a p (b , q) >>= return ∘ map₂ (_∥ r)) ≡ syncₒₖ a p (b , q ∥ r)
lemma₂ a p r (inp x) q = refl
lemma₂ a p r τ q = refl
lemma₂ a p r (out b) q = lemma₃ a p r b q (a ≟ b)
lemma : ∀ q r a p → (syncₐₒ a p q >>= return ∘ map₂ (_∥ r)) ≡ syncₐₒ a p (stepₗ q r)
lemma q r (out x) p = refl
lemma q r τ p = refl
lemma q r (inp a) p =
((q .↯ >>= syncₒₖ a p) >>= return ∘ map₂ (_∥ r)) ≡⟨ >>=-assoc _ _ _ ⟩
(q .↯ >>= (λ q′ → syncₒₖ a p q′ >>= return ∘ map₂ (_∥ r))) ≡⟨ cong (q .↯ >>=_) (funExt (uncurry (lemma₂ a p r))) ⟩
(q .↯ >>= (λ q′ → return (map₂ (_∥ r) q′) >>= syncₒₖ a p)) ≡˘⟨ >>=-assoc _ _ _ ⟩
((q .↯ >>= (return ∘ map₂ (_∥ r))) >>= syncₒₖ a p) ≡⟨⟩
(stepₗ q r .↯ >>= syncₒₖ a p) ∎
opaque
!-∥ : ∀ p → ! p ≡ p ∥ ! p
!-⌊ : ∀ p → ! p ≡ p ⌊ ! p
⌊-! : ∀ p → ! p ≡ ! p ⌊ p
!-⌊ p =
! p ≡⟨ cong-proc refl ⟩
stepₗ (p ⊕ syncᵢₒ p p) (! p) ≡⟨ cong-proc refl ⟩
stepₗ p (! p) ⊕ stepₗ (syncᵢₒ p p) (! p) ≡⟨ cong (stepₗ p (! p) ⊕_) (step-sync-assoc p p (! p)) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ≡˘⟨ ⊕𝟘 _ ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ⊕ 𝟘 ≡˘⟨ cong (stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ⊕_) (syncᵢₒ∘syncᵢₒ p p (stepₗ p (! p))) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ⊕ syncᵢₒ p (syncᵢₒ p (stepₗ p (! p))) ≡˘⟨ cong (λ e → stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ⊕ syncᵢₒ p e) (step-sync-assoc p p (! p)) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ⊕ syncᵢₒ p (stepₗ (syncᵢₒ p p) (! p)) ≡⟨ ⊕-assoc (stepₗ p (! p)) (syncᵢₒ p (stepₗ p (! p))) (syncᵢₒ p (stepₗ (syncᵢₒ p p) (! p))) ⟩
stepₗ p (! p) ⊕ (syncᵢₒ p (stepₗ p (! p)) ⊕ syncᵢₒ p (stepₗ (syncᵢₒ p p) (! p))) ≡˘⟨ cong (stepₗ p (! p) ⊕_) (syncᵢₒ-⊕ʳ _ _ _) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p) ⊕ stepₗ (syncᵢₒ p p) (! p)) ≡⟨ cong (λ e → stepₗ p (! p) ⊕ syncᵢₒ p e) (cong-proc refl) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (! p) ≡⟨ ⊕-comm (stepₗ p (! p)) (syncᵢₒ p (! p)) ⟩
syncᵢₒ p (! p) ⊕ stepₗ p (! p) ≡˘⟨ step-sync p (! p) ⟩
p ⌊ ! p ∎
⌊-! p =
! p ≡⟨ cong-proc refl ⟩
stepₗ (p ⊕ syncᵢₒ p p) (! p) ≡⟨ stepₗ-⊕ _ _ _ ⟩
stepₗ p (! p) ⊕ stepₗ (syncᵢₒ p p) (! p) ≡⟨ cong (stepₗ p (! p) ⊕_) (step-sync-assoc _ _ _) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ≡˘⟨ cong (stepₗ p (! p) ⊕_) (⊕-idem (syncᵢₒ p (stepₗ p (! p)))) ⟩
stepₗ p (! p) ⊕ (syncᵢₒ p (stepₗ p (! p)) ⊕ syncᵢₒ p (stepₗ p (! p))) ≡˘⟨ ⊕-assoc (stepₗ p (! p)) (syncᵢₒ p (stepₗ p (! p))) (syncᵢₒ p (stepₗ p (! p))) ⟩
(stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p))) ⊕ syncᵢₒ p (stepₗ p (! p)) ≡⟨ ⊕-comm (stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p))) (syncᵢₒ p (stepₗ p (! p))) ⟩
syncᵢₒ p (stepₗ p (! p)) ⊕ (stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p))) ≡˘⟨ cong₂ _⊕_ lemma₁ lemma₂ ⟩
syncᵢₒ (stepₗ (p ⊕ syncᵢₒ p p) (! p)) p ⊕ stepₗ (stepₗ (p ⊕ syncᵢₒ p p) (! p)) p ≡⟨⟩
syncᵢₒ (! p) p ⊕ stepₗ (! p) p ≡˘⟨ step-sync (! p) p ⟩
! p ⌊ p ∎
where
lemma₁ : syncᵢₒ (stepₗ (p ⊕ syncᵢₒ p p) (! p)) p ≡ syncᵢₒ p (stepₗ p (! p))
lemma₁ =
syncᵢₒ (stepₗ (p ⊕ syncᵢₒ p p) (! p)) p ≡⟨ cong (flip syncᵢₒ p) (stepₗ-⊕ _ _ _) ⟩
syncᵢₒ (stepₗ p (! p) ⊕ stepₗ (syncᵢₒ p p) (! p)) p ≡⟨ syncᵢₒ-⊕ _ _ _ ⟩
syncᵢₒ (stepₗ p (! p)) p ⊕ syncᵢₒ (stepₗ (syncᵢₒ p p) (! p)) p ≡⟨ cong (λ e → syncᵢₒ (stepₗ p (! p)) p ⊕ syncᵢₒ e p) (step-sync-assoc _ _ _) ⟩
syncᵢₒ (stepₗ p (! p)) p ⊕ syncᵢₒ (syncᵢₒ p (stepₗ p (! p))) p ≡⟨ cong (syncᵢₒ (stepₗ p (! p)) p ⊕_) (syncᵢₒ∘syncᵢₒˡ _ _ _) ⟩
syncᵢₒ (stepₗ p (! p)) p ⊕ 𝟘 ≡⟨ ⊕𝟘 _ ⟩
syncᵢₒ (stepₗ p (! p)) p ≡⟨ sync-step-assoc p (! p) p ⨾ step-sync-assoc p p (! p) ⟩
syncᵢₒ p (stepₗ p (! p)) ∎
lemma₂ : stepₗ (stepₗ (p ⊕ syncᵢₒ p p) (! p)) p ≡ stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p))
lemma₂ =
stepₗ (stepₗ (p ⊕ syncᵢₒ p p) (! p)) p ≡⟨ cong (flip stepₗ p) (stepₗ-⊕ _ _ _) ⟩
stepₗ (stepₗ p (! p) ⊕ stepₗ (syncᵢₒ p p) (! p)) p ≡⟨ stepₗ-⊕ _ _ _ ⟩
stepₗ (stepₗ p (! p)) p ⊕ stepₗ (stepₗ (syncᵢₒ p p) (! p)) p ≡⟨ cong (stepₗ (stepₗ p (! p)) p ⊕_) (cong (flip stepₗ p) (step-sync-assoc _ _ _)) ⟩
stepₗ (stepₗ p (! p)) p ⊕ stepₗ (syncᵢₒ p (stepₗ p (! p))) p ≡⟨ cong (stepₗ (stepₗ p (! p)) p ⊕_) (step-sync-assoc _ _ _) ⟩
stepₗ (stepₗ p (! p)) p ⊕ syncᵢₒ p (stepₗ (stepₗ p (! p)) p) ≡⟨ cong₂ _⊕_ (stepₗ-assoc _ _ _) (cong (syncᵢₒ p) (stepₗ-assoc _ _ _)) ⟩
stepₗ p (! p ∥ p) ⊕ syncᵢₒ p (stepₗ p (! p ∥ p)) ≡˘⟨ cong (stepₗ p (! p ∥ p) ⊕_) (step-sync-assoc _ _ _) ⟩
stepₗ p (! p ∥ p) ⊕ stepₗ (syncᵢₒ p p) (! p ∥ p) ≡˘⟨ cong₂ _⊕_ (cong (stepₗ p) (!-∥ p ⨾ ∥-comm p (! p))) (cong (stepₗ (syncᵢₒ p p)) (!-∥ p ⨾ ∥-comm p (! p) )) ⟩
stepₗ p (! p) ⊕ stepₗ (syncᵢₒ p p) (! p) ≡⟨ cong (stepₗ p (! p) ⊕_) (step-sync-assoc _ _ _) ⟩
stepₗ p (! p) ⊕ syncᵢₒ p (stepₗ p (! p)) ∎
!-∥ p =
! p ≡˘⟨ ⊕-idem (! p) ⟩
! p ⊕ ! p ≡⟨ cong₂ _⊕_ (!-⌊ p) (⌊-! p) ⟩
p ⌊ ! p ⊕ ! p ⌊ p ≡˘⟨ ⌊-∥ p (! p) ⟩
p ∥ ! p ∎
ρ-ν : ∀ ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄ (f : A → B) n p → Injective f → ρ f (ν n - p) ≡ ν f n - ρ f p
ρ-ν f n p inj = cong-proc (𝒦⟦ alg f n inj ⟧ (↯ p))
where
alg : ∀ ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄ (f : A → B) n → Injective f → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ ↯ (ρ f (ν n - ⟪ p ⟫)) ≡ ↯ (ν f n - ρ f ⟪ p ⟫)
alg f n inj .snd = prop-coh λ _ → trunc _ _
alg f n inj .fst ∅ = refl
alg f n inj .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
alg f n inj .fst ⟅ τ , p ⟆ = cong (λ e → ⟅ τ , e ⟆) (ρ-ν f n p inj)
alg f n inj .fst ⟅ out a , p ⟆ with n ≟ a | f n ≟ f a
... | yes n≡a | yes fn≡fa = refl
... | no n≢a | no fn≢fa = cong (λ e → ⟅ out (f a) , e ⟆) (ρ-ν f n p inj)
... | yes n≡a | no fn≢fa = absurd (fn≢fa (cong f n≡a))
... | no n≢a | yes fn≡fa = absurd (n≢a (inj fn≡fa))
alg f n inj .fst ⟅ inp a , p ⟆ with n ≟ a | f n ≟ f a
... | yes n≡a | yes fn≡fa = refl
... | no n≢a | no fn≢fa = cong (λ e → ⟅ inp (f a) , e ⟆) (ρ-ν f n p inj)
... | yes n≡a | no fn≢fa = absurd (fn≢fa (cong f n≡a))
... | no n≢a | yes fn≡fa = absurd (n≢a (inj fn≡fa))
procAlg : ⦃ _ : IsDiscrete A ⦄ → CCSAlg (Proc A)
procAlg = record { ProcAlg }
procMod : ⦃ _ : IsDiscrete A ⦄ → CCSSemiModel (Proc A)
procMod = record { ProcAlg ; ccsAlg = procAlg }
module _ {A : Type a} where
open import HITs.PropositionalTruncation
open import Data.Nat
Membᴺ : ℕ → A → Proc A → Type a
Membᴺ′ : ℕ → A → Act A × Proc A → Type a
Membᴺ n x xs = Any𝒦 (Membᴺ′ n x) (↯ xs)
Membᴺ′ zero x (y , _) = x ∈ₐ y
Membᴺ′ (suc n) x (_ , p) = Membᴺ n x p
open import Data.Nat.Order
Membᴺ≤ : ℕ → A → Proc A → Type a
Membᴺ≤ n a p = ∃ m × m ≤ n × Membᴺ m a p
module _ where
open ProcAlg
Memb-≤-· : ∀ {n b} a {p} → Membᴺ≤ n b p → Membᴺ≤ (suc n) b (a · p)
Memb-≤-· _ (n , prf , memb) = suc n , prf , ∣ memb ∣
Memb-≤ : ∀ {n a} {p} → Membᴺ≤ n a p → Membᴺ≤ (suc n) a p
Memb-≤ (n , prf , memb) = n , ≤-sucʳ _ _ prf , memb
Memb-≤-⊕ˡ : ∀ {n a p} q → Membᴺ≤ n a p → Membᴺ≤ n a (p ⊕ q)
Memb-≤-⊕ˡ _ (n , prf , memb) = n , prf , ∣ inl memb ∣
Memb-≤-⊕ʳ : ∀ {n a p} q → Membᴺ≤ n a p → Membᴺ≤ n a (q ⊕ p)
Memb-≤-⊕ʳ _ (n , prf , memb) = n , prf , ∣ inr memb ∣
infixr 5 _∈ᵖ_ _∉ᵖ_ _∈!ᵖ_ _∉!ᵖ_
_∈ᵖ_ _∉ᵖ_ _∈!ᵖ_ _∉!ᵖ_ : A → Proc A → Type a
x ∈!ᵖ xs = ∃ n × Membᴺ n x xs
x ∉!ᵖ xs = ¬ (x ∈!ᵖ xs)
x ∈ᵖ xs = ∥ ∃ n × Membᴺ n x xs ∥
x ∉ᵖ xs = ¬ (x ∈ᵖ xs)
module _ where
open ProcAlg
∈ᵖ-⊕ˡ : ∀ {a p} q → a ∈ᵖ p → a ∈ᵖ (p ⊕ q)
∈ᵖ-⊕ˡ _ = ∥map∥ (map₂ (∣_∣ ∘ inl))
∈ᵖ-⊕ʳ : ∀ {a q} p → a ∈ᵖ q → a ∈ᵖ (p ⊕ q)
∈ᵖ-⊕ʳ _ = ∥map∥ (map₂ (∣_∣ ∘ inr))
∈ᵖ-· : ∀ {a p} b → a ∈ᵖ p → a ∈ᵖ (b · p)
∈ᵖ-· _ = ∥map∥ (map-Σ suc ∣_∣)
isProp-∈ᵖ : ∀ x xs → isProp (x ∈ᵖ xs)
isProp-∈ᵖ x xs = squash
∈ᵃ→𝒦⇒P : ∀ s a p ps → (emit s a , p) 𝒦∈ ↯ ps → a ∈ᵖ ps
∈ᵃ→𝒦⇒P s a p ps sp∈ps = ∣ zero , 𝒦-weaken-any (λ { {emit s b , p} eq → emit-inj (cong fst eq) ; {τ , p} eq → absurd (τ≢emit (sym (cong fst eq))) }) (↯ ps) sp∈ps ∣
∈ᵖ→𝒦⇒P : ∀ s a p ps → (s , p) 𝒦∈ ↯ ps → a ∈ᵖ p → a ∈ᵖ ps
∈ᵖ→𝒦⇒P s a p ps sp∈ps = ∥map∥ (map-Σ suc λ a∈p → 𝒦-weaken-any ( λ eq → subst (Membᴺ _ a) (cong snd eq) a∈p) (↯ ps) sp∈ps)
module _ {B : Type b} where
ρ-with-∈ : (xs : Proc A) → (∀ x → x ∈ᵖ xs → B) → Proc B
ρ-with-∈′ : (xs : Proc A) → (∀ x → x ∈ᵖ xs → B) → (x : Act A × Proc A) → x 𝒦∈ ↯ xs → Act B × Proc B
ρ-with-∈ xs f = ⟪ 𝒦-map-with-∈ (↯ xs) (ρ-with-∈′ xs f) ⟫
ρ-with-∈′ xs f (emit s a , p) x∈xs = emit s (f a (∈ᵃ→𝒦⇒P s a p xs x∈xs)) , ρ-with-∈ p λ b b∈ → f b (∈ᵖ→𝒦⇒P (emit s a) b p xs x∈xs b∈)
ρ-with-∈′ xs f (τ , p) x∈xs = τ , ρ-with-∈ p λ a a∈ → f a (∈ᵖ→𝒦⇒P τ a p xs x∈xs a∈)
open ProcAlg using (ρ; ρ$)
ρ-without-∈ : (f : A → B) (xs : Proc A) → ρ-with-∈ xs (const ∘′ f) ≡ ρ f xs
ρ-without-∈ f xs =
ρ-with-∈ xs (const ∘′ f) ≡⟨ cong-proc refl ⟩
⟪ 𝒦-map-with-∈ (↯ xs) (ρ-with-∈′ xs (const ∘′ f)) ⟫ ≡⟨ cong-proc (cong (𝒦-map-with-∈ (↯ xs))
(funExt λ { (τ , p) → funExt λ _ → cong (τ ,_) (ρ-without-∈ f p)
; (emit s b , p) → funExt λ _ → cong (emit s (f b) ,_) (ρ-without-∈ f p) })) ⟩
⟪ 𝒦-map-with-∈ (↯ xs) (const ∘′ map-Σ (map-act f) (ρ f)) ⟫ ≡⟨ cong-proc (𝒦-map-with-∈-map _ (↯ xs)) ⟩
⟪ 𝒦-map (map-Σ (map-act f) (ρ f)) (↯ xs) ⟫ ≡⟨ cong-proc refl ⟩
ρ f xs ∎
open ProcAlg
using
( _⌊ₖ_
; syncₒₖ
; syncₒ
; syncₐₒ
; stepₗ-⊕
; syncᵢₒ
; stepₗ
; ν′
; steps
; stepsₗ
; step-sync
; syncᵢₒ-⊕ʳ
; syncᵢₒ-assoc
; syncᵢₒ-match
; syncᵢₒ-nomatch
; step-is-step
; sync𝟘ʳ
; ρ
; ρ-ν
; ρ$
) public
private module Rho where
open CCSAlg ⦃ ... ⦄
open CCSSemiModel ⦃ ... ⦄
instance
ccsAlgProc : ⦃ _ : IsDiscrete A ⦄ → CCSAlg (Proc A)
ccsAlgProc = procAlg
instance
ccsProc : ⦃ _ : IsDiscrete A ⦄ → CCSSemiModel (Proc A)
ccsProc = procMod
module _ {A : Type a} ⦃ _ : IsDiscrete A ⦄ where
⟦_⟧ᵖ : P A → Proc A
⟦_⟧ᵖ = ⟦_⟧
open import HITs.PropositionalTruncation
open import Truth hiding (_∥_)
ν⇒Memb : ∀ (n m : A) o p → Membᴺ o n (ν m - p) → Membᴺ o n p
ν⇒Memb n m o p = 𝒦⟦ alg n m o ⟧ (↯ p)
where
alg : ∀ (n m : A) o → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ o n (ν m - ⟪ p ⟫) → Membᴺ o n ⟪ p ⟫)
alg n m o .snd = prop-coh λ p → isProp→ (isProp-Any _ p)
alg n m o .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥map∥ (map-⊎ P⟨xs⟩ P⟨ys⟩)
alg n m zero .fst ⟅ τ , p ⟆ = ∥rec∥ squash Poly-absurd
alg n m (suc o) .fst ⟅ τ , p ⟆ = ∥map∥ (ν⇒Memb n m o p)
alg n m o .fst ⟅ emit s b , p ⟆ n∈p with m ≟ b
alg n m zero .fst ⟅ emit s b , p ⟆ n∈p | no m≢b = n∈p
alg n m (suc o) .fst ⟅ emit s b , p ⟆ n∈p | no m≢b = ∥map∥ (ν⇒Memb n m o p) n∈p
open import Swaps {A = A}
Memb⁰-step : ∀ (a : A) p q → Membᴺ zero a p ⟷ Membᴺ zero a (stepₗ p q)
Memb⁰-step a p q = 𝒦⟦ alg a q ⟧ (↯ p)
where
alg : ∀ (a : A) q → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ zero a ⟪ p ⟫ ⟷ Membᴺ zero a (stepₗ ⟪ p ⟫ q))
alg a q .snd = prop-coh λ p → isProp× (isProp→ (isProp-Any _ (↯ (stepₗ ⟪ p ⟫ q)))) (isProp→ (isProp-Any _ p))
alg a q .fst ⟅ b , p ⟆ .fst = id
alg a q .fst ⟅ b , p ⟆ .snd = id
alg a q .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) .fst = ∥map∥ (map-⊎ (fst P⟨xs⟩) (fst P⟨ys⟩))
alg a q .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) .snd = ∥map∥ (map-⊎ (snd P⟨xs⟩) (snd P⟨ys⟩))
¬Memb⁰-sync : ∀ (a : A) p q → ¬ (Membᴺ zero a (syncᵢₒ p q))
¬Memb⁰-sync a p q = 𝒦⟦ alg a q ⟧ (↯ p)
where
lemma : ∀ (a : A) bc (p : Proc A) → ¬ Any𝒦 (λ q → a ∈ₐ fst (q ⦂ Act A × Proc A)) (bc guarding ⟅ τ , p ⟆)
lemma a true p = ∥rec∥ isProp⊥ Poly-absurd
alg₂ : ∀ a b p → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ ¬ Any𝒦 (((a ∈ₐ_) ∘ fst)) ((syncₒ b p ⟪ q ⟫))
alg₂ a b p .snd = prop-coh λ _ → isProp→ isProp⊥
alg₂ a b p .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ isProp⊥ (P⟨xs⟩ ▿ P⟨ys⟩)
alg₂ a b p .fst ⟅ out c , q ⟆ a∈r = lemma a (does (b ≟ c)) (p ∥ q) a∈r
alg : ∀ a q → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ ¬ Any𝒦 ( ((a ∈ₐ_) ∘ fst)) (↯ (syncᵢₒ ⟪ p ⟫ q))
alg a q .snd = prop-coh λ _ → isProp→ isProp⊥
alg a q .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ isProp⊥ (P⟨xs⟩ ▿ P⟨ys⟩)
alg a q .fst ⟅ inp b , p ⟆ = 𝒦⟦ alg₂ a b p ⟧ (↯ q)
⌊⇒∈ᵖ : ∀ (a : A) p q n → Membᴺ n a (p ⌊ q) → ∥ Membᴺ≤ n a p ⊎ Membᴺ≤ n a q ∥
⌊⇒∈ᵖ a p q n = 𝒦⟦ alg a q n ⟧ (↯ p)
where
alg₂ : ∀ n a b p → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ n a ⟪ syncₒ b p ⟪ q ⟫ ⟫ → ∥ Membᴺ≤ n a ⟪ ⟅ inp b , p ⟆ ⟫ ⊎ Membᴺ≤ n a ⟪ q ⟫ ∥)
alg₂ n a b p .snd = prop-coh λ q → isProp→ squash
alg₂ n a b p .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ squash (∥map∥ (mapʳ (Memb-≤-⊕ˡ ⟪ ys ⟫)) ∘ P⟨xs⟩ ▿ ∥map∥ (mapʳ (Memb-≤-⊕ʳ ⟪ xs ⟫)) ∘ P⟨ys⟩)
alg₂ n a b p .fst ⟅ out c , q ⟆ with b ≟ c
... | no b≢c = Poly-absurd
alg₂ zero a b p .fst ⟅ out c , q ⟆ | yes b≡c = ∥rec∥ squash Poly-absurd
alg₂ (suc n) a b p .fst ⟅ out c , q ⟆ | yes b≡c = ∥rec∥ squash (∥rec∥ squash
((∥map∥ (map-⊎ (Memb-≤-· (inp b)) (Memb-≤-· (out c))) ∘ ⌊⇒∈ᵖ a p q n) ▿
∥map∥ (inr ∘ Memb-≤-· (out c) ▿ inl ∘ Memb-≤-· (inp b)) ∘ ⌊⇒∈ᵖ a q p n) ∘ subst (Membᴺ n a) (⌊-∥ p q))
lemma₁ : ∀ n (a : A) b p q → ∥ Membᴺ′ n a (b , p ∥ q) ∥ → ∥ Membᴺ≤ n a ⟪ ⟅ b , p ⟆ ⟫ ⊎ Membᴺ≤ n a q ∥
lemma₁ zero a b p q = ∥map∥ (inl ∘ (zero ,_) ∘ (tt ,_) ∘ ∣_∣)
lemma₁ (suc n) a b p q =
∥rec∥ squash
(∥rec∥ squash (∥map∥ (map-⊎ (Memb-≤-· b) Memb-≤) ∘ ⌊⇒∈ᵖ a p q n ▿ ∥map∥
(inr ∘ Memb-≤ ▿ inl ∘ Memb-≤-· b ) ∘ ⌊⇒∈ᵖ a q p n) ∘ subst (Membᴺ n a) (⌊-∥ p q))
lemma₂ : ∀ n a b p q → Membᴺ n a ⟪ syncₐₒ b p q ⟫ → ∥ Membᴺ≤ n a ⟪ ⟅ b , p ⟆ ⟫ ⊎ Membᴺ≤ n a q ∥
lemma₂ n a (inp b) p q = 𝒦⟦ alg₂ n a b p ⟧ (↯ q)
alg : ∀ a q n → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ n a (⟪ p ⟫ ⌊ q) → ∥ Membᴺ≤ n a ⟪ p ⟫ ⊎ Membᴺ≤ n a q ∥)
alg a q n .snd = prop-coh λ p → isProp→ squash
alg a q n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ squash (∥map∥ (mapˡ (map₂ (map₂ (∣_∣ ∘ inl)))) ∘ P⟨xs⟩ ▿ ∥map∥ (mapˡ (map₂ (map₂ (∣_∣ ∘ inr)))) ∘ P⟨ys⟩)
alg a q n .fst ⟅ b , p ⟆ = ∥rec∥ squash (lemma₂ n a b p q ▿ lemma₁ n a b p q)
∥⇒∈ᵖ : ∀ (a : A) p q n → Membᴺ n a (p ∥ q) → ∥ Membᴺ≤ n a p ⊎ Membᴺ≤ n a q ∥
∥⇒∈ᵖ a p q n = ∥rec∥ squash ( ⌊⇒∈ᵖ a p q n ▿ ∥map∥ (inr ▿ inl) ∘ ⌊⇒∈ᵖ a q p n) ∘ subst (Membᴺ n a) (⌊-∥ p q)
step⇒∈ᵖ : ∀ (a : A) p q n → Membᴺ (suc n) a (stepₗ p q) → ∥ Membᴺ≤ (suc n) a p ⊎ Membᴺ≤ n a q ∥
step⇒∈ᵖ a p q n = 𝒦⟦ alg a q n ⟧ (↯ p)
where
alg : ∀ (a : A) q n → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ (suc n) a (stepₗ ⟪ p ⟫ q) → ∥ Membᴺ≤ (suc n) a ⟪ p ⟫ ⊎ Membᴺ≤ n a q ∥)
alg a q n .snd = prop-coh λ p → isProp→ squash
alg a q n .fst ⟅ b , p ⟆ = ∥rec∥ squash ( ∥map∥ (map-⊎ (Memb-≤-· b) id) ∘ ∥⇒∈ᵖ a p q n)
alg a q n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ squash (∥map∥ (mapˡ (Memb-≤-⊕ˡ ⟪ ys ⟫)) ∘ P⟨xs⟩ ▿ ∥map∥ (mapˡ (Memb-≤-⊕ʳ ⟪ xs ⟫)) ∘ P⟨ys⟩)
sync⇒∈ᵖ : ∀ (a : A) p q n → Membᴺ n a (syncᵢₒ p q) → ∥ Membᴺ≤ n a p ⊎ Membᴺ≤ n a q ∥
sync⇒∈ᵖ a p q n = 𝒦⟦ alg a q n ⟧ (↯ p)
where
alg₂ : ∀ (a b : A) p n → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ n a ⟪ syncₒ b p ⟪ q ⟫ ⟫ → ∥ Membᴺ≤ n a ⟪ ⟅ inp b , p ⟆ ⟫ ⊎ Membᴺ≤ n a ⟪ q ⟫ ∥)
alg₂ a b p n .snd = prop-coh λ p → isProp→ squash
alg₂ a b p n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ squash (∥map∥ (mapʳ (Memb-≤-⊕ˡ ⟪ ys ⟫)) ∘ P⟨xs⟩ ▿ ∥map∥ (mapʳ (Memb-≤-⊕ʳ ⟪ xs ⟫)) ∘ P⟨ys⟩)
alg₂ a b p n .fst ⟅ out c , q ⟆ with b ≟ c
alg₂ a b p zero .fst ⟅ out c , q ⟆ | yes b≡c = ∥rec∥ squash Poly-absurd
alg₂ a b p (suc n) .fst ⟅ out c , q ⟆ | yes b≡c = ∥rec∥ squash ( ∥map∥ (map-⊎ (Memb-≤-· (inp b)) (Memb-≤-· (out c))) ∘ ∥⇒∈ᵖ a p q n)
alg : ∀ (a : A) q n → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (Membᴺ n a (syncᵢₒ ⟪ p ⟫ q) → ∥ Membᴺ≤ n a ⟪ p ⟫ ⊎ Membᴺ≤ n a q ∥)
alg a q n .snd = prop-coh λ p → isProp→ squash
alg a q n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = ∥rec∥ squash (∥map∥ (mapˡ (Memb-≤-⊕ˡ ⟪ ys ⟫)) ∘ P⟨xs⟩ ▿ ∥map∥ (mapˡ (Memb-≤-⊕ʳ ⟪ xs ⟫)) ∘ P⟨ys⟩)
alg a q n .fst ⟅ inp b , p ⟆ = 𝒦⟦ alg₂ a b p n ⟧ (↯ q)
!⇒∈ᵖ : ∀ (a : A) p n → Membᴺ n a (! p) → a ∈ᵖ p
!⇒∈ᵖ a p zero = ∥rec∥ squash (∣_∣ ∘ (zero ,_) ∘ Memb⁰-step a p (! p) .snd ▿ absurd ∘ ¬Memb⁰-sync a p p ∘ Memb⁰-step a (syncᵢₒ p p) (! p) .snd ) ∘ subst (Membᴺ zero a) (cong-proc refl ⨾ stepₗ-⊕ p (syncᵢₒ p p) (! p))
!⇒∈ᵖ a p (suc n) = ∥rec∥ squash (lemma₁ a p n ▿ lemma₂ a p n) ∘ subst (Membᴺ (suc n) a) (cong-proc refl ⨾ stepₗ-⊕ p (syncᵢₒ p p) (! p))
where
lemma₁ : ∀ a p n → Membᴺ (suc n) a (stepₗ p (! p)) → a ∈ᵖ p
lemma₁ a p n a∈sp = 𝒦⟦ alg₁ a p n ⟧ (↯ p) (subst (a ∈ᵖ_) (proc∘↯ _)) (subst (λ p′ → Membᴺ (suc n) a (stepₗ p′ (! p))) (sym (proc∘↯ p)) a∈sp)
where
alg₁ : ∀ a q n → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ ((a ∈ᵖ ⟪ p ⟫ → a ∈ᵖ q) → Membᴺ (suc n) a (stepₗ ⟪ p ⟫ (! q)) → a ∈ᵖ q)
alg₁ a q n .snd = prop-coh λ p → isProp→ (isProp→ squash)
alg₁ a q n .fst ⟅ b , p ⟆ k = ∥rec∥ squash ( ∥rec∥ squash ( (k ∘ ∈ᵖ-· b ∘ ∣_∣ ∘ (_ ,_) ) ∘′ snd ∘′ snd ▿ !⇒∈ᵖ a q _ ∘′ snd ∘′ snd ) ∘ ∥⇒∈ᵖ a p (! q) n)
alg₁ a q n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) k = ∥rec∥ squash (P⟨xs⟩ (k ∘ ∈ᵖ-⊕ˡ ⟪ ys ⟫) ▿ P⟨ys⟩ (k ∘ ∈ᵖ-⊕ʳ ⟪ xs ⟫))
lemma₂ : ∀ a p n → Membᴺ (suc n) a (stepₗ (syncᵢₒ p p) (! p)) → a ∈ᵖ p
lemma₂ a p n = ∥rec∥ squash ( ( ∥map∥ ((_ ,_) ∘′ snd ∘′ snd ▿ (_ ,_) ∘′ snd ∘′ snd) ∘ sync⇒∈ᵖ a p p _) ∘′ snd ∘′ snd ▿ !⇒∈ᵖ a p _ ∘′ snd ∘′ snd) ∘ step⇒∈ᵖ a (syncᵢₒ p p) (! p) n
∈ₚ⇒∈ᵖ : ∀ (a : A) p → a ∈ᵖ ⟦ p ⟧ → ∥ a ∈ₚ p ∥
∈ₚ⇒∈ᵖ a p = ∥rec∥ squash (uncurry (lemma a p))
where
lemma : ∀ (a : A) p n → Membᴺ n a ⟦ p ⟧ → ∥ a ∈ₚ p ∥
lemma a (p `⌊ q) n = ∥rec∥ squash ((∥map∥ inl ∘ lemma a p _ ∘′ snd ∘′ snd) ▿ (∥map∥ inr ∘ lemma a q _ ∘′ snd ∘′ snd)) ∘ ⌊⇒∈ᵖ a ⟦ p ⟧ ⟦ q ⟧ n
lemma a (b `· p) zero = ∥map∥ inl
lemma a (b `· p) (suc n) = ∥rec∥ squash (∥map∥ inr ∘ lemma a p n)
lemma a (p `⊕ q) n = ∥rec∥ squash (∥map∥ inl ∘ lemma a p n ▿ ∥map∥ inr ∘ lemma a q n)
lemma a (p `∥ q) n = ∥rec∥ squash (∥map∥ (map-⊎ id id) ∘ lemma a (p ⌊ q) n ▿ ∥map∥ (inr ▿ inl) ∘ lemma a (q ⌊ p) n) ∘ subst (Membᴺ n a) (⌊-∥ ⟦ p ⟧ ⟦ q ⟧)
lemma a (`ν b - p) n = ∥map∥ inr ∘ lemma a p n ∘ ν⇒Memb a b n ⟦ p ⟧
lemma a (`! p) n = ∥rec∥ squash (uncurry (lemma a p) ) ∘ !⇒∈ᵖ a ⟦ p ⟧ n
∉ᵖ⇒∉ₚ : ∀ (a : A) p → a ∉ₚ p → a ∉ᵖ ⟦ p ⟧
∉ᵖ⇒∉ₚ a p a∉p a∈p = ∥rec∥ isProp⊥ a∉p (∈ₚ⇒∈ᵖ a p a∈p)
syncᵢₒ-rewrite : ∀ (n : List A) (a : Act A) p q → νₛ n - syncᵢₒ (a · p) (! q) ≡ νₛ n - syncᵢₒ (a · (p ∥ ! q)) q
syncᵢₒ-rewrite n a p q = cong (νₛ n -_) (cong (syncᵢₒ (a · p)) (!-⌊ q) ⨾ sym (ProcAlg.syncᵢₒ-assoc a p (! q) q))
ν-∉ᵖ : ∀ (n : A) p → n ∉ᵖ p → ν n - p ≡ p
ν-∉ᵖ n p n∉p = cong (ν n -_) (sym (proc∘↯ p)) ⨾ 𝒦⟦ alg n ⟧ (↯ p) n∉p ⨾ proc∘↯ p
where
alg : ∀ (n : A) → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (n ∉ᵖ ⟪ p ⟫ → ν n - ⟪ p ⟫ ≡ ⟪ p ⟫)
alg n .snd = prop-coh λ p → isProp→ (isSetProc _ _)
alg n .fst ∅ n∉p = cong-proc refl
alg n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) n∉p = ν-⊕ n ⟪ xs ⟫ ⟪ ys ⟫ ⨾ cong₂ _⊕_ (P⟨xs⟩ (n∉p ∘ ∈ᵖ-⊕ˡ ⟪ ys ⟫)) (P⟨ys⟩ (n∉p ∘ ∈ᵖ-⊕ʳ ⟪ xs ⟫))
alg n .fst ⟅ τ , p ⟆ n∉p = cong-proc refl ⨾ cong (τ ·_) (ν-∉ᵖ n p (n∉p ∘ ∈ᵖ-· τ))
alg n .fst ⟅ emit s m , p ⟆ n∉p with n ≟ m
... | yes n≡m = absurd (n∉p ∣ zero , ∣ n≡m ∣ ∣)
... | no n≢m = cong-proc (cong (maybe′ ∅ ⟅_⟆ ∘ bool _ _) (it-doesn't (n ≟ m) n≢m)) ⨾ cong (emit s m ·_) (ν-∉ᵖ n p (n∉p ∘ ∈ᵖ-· (emit s m)))
ν-ρ-∉ᵖ : ∀ (n m : A) p → m ∉ᵖ p → ν n - p ≡ ν m - ρ (n /↔ m) p
ν-ρ-∉ᵖ n m p m∉p = cong (ν n -_) (cong-proc refl) ⨾ 𝒦⟦ alg n m ⟧ (↯ p) m∉p ⨾ cong-proc refl
where
alg : ∀ (n m : A) → Ψ[ p ⦂ 𝒦 (Act A × Proc A) ] ↦ (m ∉ᵖ ⟪ p ⟫ → ν n - ⟪ p ⟫ ≡ ν m - ρ (n /↔ m) ⟪ p ⟫)
alg n m .snd = prop-coh λ p → isProp→ (isSetProc _ _)
alg n m .fst ∅ m∉p = cong-proc refl
alg n m .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) m∉p =
ν n - ⟪ xs ∪ ys ⟫ ≡⟨ cong-proc refl ⟩
ν n - ⟪ xs ⟫ ⊕ ν n - ⟪ ys ⟫ ≡⟨ cong₂ _⊕_ (P⟨xs⟩ (m∉p ∘ ∈ᵖ-⊕ˡ ⟪ ys ⟫)) (P⟨ys⟩ (m∉p ∘ ∈ᵖ-⊕ʳ ⟪ xs ⟫)) ⟩
ν m - ρ (n /↔ m) ⟪ xs ⟫ ⊕ ν m - ρ (n /↔ m) ⟪ ys ⟫ ≡⟨ cong-proc refl ⟩
ν m - ρ (n /↔ m) ⟪ xs ∪ ys ⟫ ∎
alg n m .fst ⟅ τ , p ⟆ m∉p = cong-proc refl ⨾ cong (τ ·_) (ν-ρ-∉ᵖ n m p (m∉p ∘ ∈ᵖ-· τ)) ⨾ cong-proc refl
alg n m .fst ⟅ emit s o , p ⟆ m∉p with n ≟ o | m ≟ o
... | yes n≡o | _ =
ν n - ⟪ ⟅ emit s o , p ⟆ ⟫ ≡⟨ cong-proc (cong (⟅?⟆ ∘ bool _ _) (it-does (n ≟ o) n≡o)) ⟩
𝟘 ≡˘⟨ cong-proc (cong (⟅?⟆ ∘ bool _ _) (it-does (m ≟ m) refl)) ⟩
ν m - ⟪ ⟅ emit s m , ρ (n /↔ m) p ⟆ ⟫ ≡˘⟨ cong (λ e → ν m - ⟪ ⟅ emit s e , ρ (n /↔ m) p ⟆ ⟫) (cong (bool _ _) (it-does (o ≟ n) (sym n≡o))) ⟩
ν m - ⟪ ⟅ emit s ((n /↔ m) o) , ρ (n /↔ m) p ⟆ ⟫ ≡⟨ cong-proc refl ⟩
ν m - ρ (n /↔ m) ⟪ ⟅ emit s o , p ⟆ ⟫ ∎
... | _ | yes m≡o = absurd (m∉p ∣ zero , ∣ m≡o ∣ ∣)
... | no n≢o | no m≢o =
ν n - ⟪ ⟅ emit s o , p ⟆ ⟫ ≡⟨ cong-proc (cong (⟅?⟆ ∘ bool _ _) (it-doesn't (n ≟ o) n≢o)) ⟩
⟪ ⟅ emit s o , ν n - p ⟆ ⟫ ≡⟨ cong (emit s o ·_) (ν-ρ-∉ᵖ n m p (m∉p ∘ ∈ᵖ-· (emit s o))) ⟩
⟪ ⟅ emit s o , ν m - ρ (n /↔ m) p ⟆ ⟫ ≡˘⟨ cong-proc (cong (⟅?⟆ ∘ bool _ _) (it-doesn't (m ≟ o) m≢o)) ⟩
ν m - ⟪ ⟅ emit s o , ρ (n /↔ m) p ⟆ ⟫ ≡˘⟨ cong (λ e → ν m - ⟪ ⟅ emit s e , ρ (n /↔ m) p ⟆ ⟫) (swap-neq n m o n≢o m≢o) ⟩
ν m - ⟪ ⟅ emit s ((n /↔ m) o) , ρ (n /↔ m) p ⟆ ⟫ ≡⟨ cong-proc refl ⟩
ν m - ρ (n /↔ m) ⟪ ⟅ emit s o , p ⟆ ⟫ ∎
module _ {A : Type a} {B : Type b} ⦃ _ : IsDiscrete A ⦄ ⦃ _ : IsDiscrete B ⦄ (f↣ : A ↣ B) where
private
f = fst f↣
fi = snd f↣
mutual
syncₐₒ-map : ∀ a p q →
syncₐₒ a p q >>- ρ$ f ≡ syncₐₒ (map-act f a) (ρ f p) (ρ f q)
syncₐₒ-map (out _) p q = refl
syncₐₒ-map τ p q = refl
syncₐₒ-map (inp a) p q =
syncₒ a p q >>- ρ$ f ≡⟨⟩
(↯ q >>= syncₒₖ a p) >>- ρ$ f ≡⟨ >>=-assoc _ _ _ ⟩
↯ q >>= (λ q′ → syncₒₖ a p q′ >>- ρ$ f) ≡⟨ cong (↯ q >>=_) (funExt (uncurry (syncₒₖ-map a p))) ⟩
↯ q >>= (syncₒₖ (f a) (ρ f p) ∘ ρ$ f) ≡˘⟨ >>=-assoc _ _ _ ⟩
(↯ q >>- ρ$ f) >>= syncₒₖ (f a) (ρ f p) ≡⟨⟩
syncₒ (f a) (ρ f p) (ρ f q) ∎
syncₒₖ-map : ∀ a p b q →
syncₒₖ a p (b , q) >>- ρ$ f ≡ syncₒₖ (f a) (ρ f p) (map-act f b , ρ f q)
syncₒₖ-map a p (inp _) q = refl
syncₒₖ-map a p τ q = refl
syncₒₖ-map a p (out b) q =
guarding->>= (does (a ≟ b)) _ _ ⨾ cong₃ bool refl (cong (⟅_⟆ ∘ (_,_ τ)) (ρ-∥ p q)) (both-do (a ≟ b) (f a ≟ f b) (cong f , fi))
ρ-∥ : ∀ p q → ρ f (p ∥ q) ≡ ρ f p ∥ ρ f q
ρ-∥ p q =
ρ f (p ∥ q) ≡⟨ cong (ρ f) (cong-proc refl) ⟩
ρ f ((p ⌊ q) ⊕ (q ⌊ p)) ≡⟨ cong-proc refl ⟩
ρ f (p ⌊ q) ⊕ ρ f (q ⌊ p) ≡⟨ cong₂ _⊕_ (ρ-⌊ p q) (ρ-⌊ q p) ⨾ cong-proc refl ⟩
ρ f p ∥ ρ f q ∎
⌊ₖ-map : ∀ q p →
(p ⌊ₖ q) >>- ρ$ f ≡ map-Σ (map-act f) (ρ f) p ⌊ₖ ρ f q
⌊ₖ-map q (a , p) =
((a , p) ⌊ₖ q) >>- ρ$ f ≡⟨⟩
(syncₐₒ a p q ∪ ⟅ a , (p ∥ q) ⟆) >>- ρ$ f ≡⟨⟩
(syncₐₒ a p q >>- ρ$ f) ∪ ⟅ map-act f a , ρ f (p ∥ q) ⟆ ≡⟨ cong₂ _∪_ (syncₐₒ-map a p q) (cong (⟅_⟆ ∘ _,_ (map-act f a)) (ρ-∥ p q)) ⟩
syncₐₒ (map-act f a) (ρ f p) (ρ f q) ∪ ⟅ map-act f a , (ρ f p ∥ ρ f q) ⟆ ≡⟨⟩
(map-act f a , ρ f p) ⌊ₖ ρ f q ∎
ρ-⌊ : ∀ p q → ρ f (p ⌊ q) ≡ ρ f p ⌊ ρ f q
ρ-⌊ p q =
ρ f (p ⌊ q) ≡⟨ cong-proc refl ⟩
⟪ ↯ (p ⌊ q) >>- ρ$ f ⟫ ≡⟨⟩
⟪ (↯ p >>= (_⌊ₖ q)) >>- ρ$ f ⟫ ≡⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ ↯ p >>= (λ p′ → (p′ ⌊ₖ q) >>- ρ$ f ) ⟫ ≡⟨ cong-proc (cong (↯ p >>=_) (funExt (⌊ₖ-map q))) ⟩
⟪ ↯ p >>= (λ p′ → ⟅ map-Σ (map-act f) (ρ f) p′ ⟆ >>= (_⌊ₖ ρ f q)) ⟫ ≡˘⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ (↯ p >>- ρ$ f) >>= (_⌊ₖ ρ f q) ⟫ ≡⟨⟩
⟪ ↯ (ρ f p) >>= (_⌊ₖ ρ f q) ⟫ ≡⟨ cong-proc refl ⟩
ρ f p ⌊ ρ f q ∎
ρ-hom : ∀ p → ρ f ⟦ p ⟧ ≡ ⟦ `ρ f p ⟧
ρ-hom `𝟘 = cong-proc refl
ρ-hom (p `⊕ q) = cong-proc refl ⨾ cong₂ _⊕_ (ρ-hom p) (ρ-hom q)
ρ-hom (p `∥ q) =
ρ f ⟦ p `∥ q ⟧ ≡⟨ cong (ρ f) (cong-proc refl) ⟩
ρ f ⟦ (p `⌊ q) `⊕ (q `⌊ p) ⟧ ≡⟨ cong-proc refl ⨾ cong₂ _⊕_ (ρ-hom (p `⌊ q)) (ρ-hom (q `⌊ p)) ⟩
⟦ `ρ f ((p `⌊ q) `⊕ (q `⌊ p)) ⟧ ≡⟨ cong-proc refl ⟩
⟦ `ρ f (p `∥ q) ⟧ ∎
ρ-hom (a `· p) = cong-proc (cong ⟅_⟆ (cong₂ _,_ refl (ρ-hom p)))
ρ-hom (`! p) =
ρ f ⟦ ! p ⟧ ≡⟨ cong (ρ f) (!-⌊ ⟦ p ⟧) ⟩
ρ f ⟦ p ⌊ ! p ⟧ ≡⟨ ρ-hom (p ⌊ ! p) ⟩
⟦ `ρ f (p ⌊ ! p) ⟧ ≡˘⟨ !-⌊ _ ⟩
⟦ `ρ f (! p) ⟧ ∎
ρ-hom (`ν n - p) =
ρ f ⟦ ν n - p ⟧ ≡⟨⟩
ρ f (ν n - ⟦ p ⟧) ≡⟨ ρ-ν f n ⟦ p ⟧ fi ⟩
ν f n - ρ f ⟦ p ⟧ ≡⟨ cong (ν f n -_) (ρ-hom p) ⟩
ν f n - ⟦ `ρ f p ⟧ ∎
ρ-hom (p `⌊ q) =
ρ f ⟦ p ⌊ q ⟧ ≡⟨ cong-proc refl ⟩
⟪ ↯ ⟦ p ⌊ q ⟧ >>- ρ$ f ⟫ ≡⟨⟩
⟪ (↯ ⟦ p ⟧ >>= (_⌊ₖ ⟦ q ⟧)) >>- ρ$ f ⟫ ≡⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ ↯ ⟦ p ⟧ >>= (λ p′ → p′ ⌊ₖ ⟦ q ⟧ >>- ρ$ f) ⟫ ≡⟨ cong-proc (cong (↯ ⟦ p ⟧ >>=_) (funExt (⌊ₖ-map ⟦ q ⟧))) ⟩
⟪ ↯ ⟦ p ⟧ >>= (λ p′ → ⟅ map-Σ (map-act f) (ρ f) p′ ⟆ >>= (_⌊ₖ ρ f ⟦ q ⟧)) ⟫ ≡˘⟨ cong-proc (>>=-assoc _ _ _) ⟩
⟪ (↯ ⟦ p ⟧ >>- ρ$ f) >>= (_⌊ₖ ρ f ⟦ q ⟧) ⟫ ≡⟨⟩
⟪ ↯ (ρ f ⟦ p ⟧) >>= (_⌊ₖ ρ f ⟦ q ⟧) ⟫ ≡⟨ cong-proc refl ⟩
ρ f ⟦ p ⟧ ⌊ ρ f ⟦ q ⟧ ≡⟨ cong₂ _⌊_ (ρ-hom p) (ρ-hom q) ⟩
⟦ `ρ f p ⟧ ⌊ ⟦ `ρ f q ⟧ ≡⟨⟩
⟦ `ρ f p ⌊ `ρ f q ⟧ ∎
open Rho using
( syncᵢₒ-rewrite
; ρ-hom
; ν-∉ᵖ
; ∉ᵖ⇒∉ₚ
; ∈ₚ⇒∈ᵖ
; ν-ρ-∉ᵖ
) public