{-# OPTIONS --no-termination-check #-}
open import Prelude hiding (P; A)
module CCS.Homomorphism.CtoP where
open import CCS.Alg
open import CCS.SemiModel
import CCS.Proc as β
open import Algebra
open β using (Proc; procAlg; procMod; cong-proc)
open import Data.Set renaming (β¦_β§ to π¦β¦_β§)
private
A : Type
A = β
open import Hyper.Base
open import CCS.Hyp.Definition A (Proc A)
open CCSAlg β¦ ... β¦
open CCSSemiModel β¦ ... β¦
instance
_ : CCSAlg (Proc A)
_ = procAlg
instance
_ : CCSSemiModel (Proc A)
_ = procMod
open import CCS.Hyp.Properties {R = Proc A} procMod hiding (ββ)
instance
_ : CCSAlg Communicator
_ = hypAlg
instance
_ : CCSSemiModel Communicator
_ = hypMod
open import CCS.Hyp.Interp {R = Proc A} procAlg β¦ it β¦
open import CCS.Fresh.Hyp
import CCS.Fresh.Proc as β
open import CCS.Fresh
open import Swaps {A = A}
β-homβ : (n : List A) (p q : P A) β β¦ Ξ½β n - β¦ p β q β§ β§β β‘ Ξ½β n - β¦ p β q β§
β₯-homβ : (n : List A) (p q : P A) β β¦ Ξ½β n - β¦ p β₯ q β§ β§β β‘ Ξ½β n - β¦ p β₯ q β§
sync-homβ : (n : List A) (a : Act A) (p q : P A) β β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ q β§ β§β β‘ Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ q β§
step-homβ : (n : List A) (a : Act A) (p q : P A) β β¦ Ξ½β n - β¦ a Β· (p β₯ q) β§ β§β β‘ Ξ½β n - β.stepβ β¦ a Β· p β§ β¦ q β§
π-homβ : β (n : List A) (p : Communicator) (q : Proc A)
β p β‘ π
β q β‘ π
β β¦ Ξ½β n - p β§β β‘ Ξ½β n - q
π-homβ n p q c0 p0 =
β¦ Ξ½β n - p β§β β‘β¨ cong (β¦_β§β β (Ξ½β n -_)) c0 β©
β¦ Ξ½β n - π β§β β‘β¨ cong β¦_β§β (Ξ½β-π n) β©
β¦ π β§β β‘β¨β©
π β‘Λβ¨ Ξ½β-π n β©
Ξ½β n - π β‘Λβ¨ cong (Ξ½β n -_) p0 β©
Ξ½β n - q β
β₯-homβ n p q =
β¦ Ξ½β n - β¦ p β₯ q β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-β n _ _) β©
β¦ Ξ½β n - β¦ p β q β§ β§β β β¦ Ξ½β n - β¦ q β p β§ β§β β‘β¨ congβ _β_ (β-homβ n p q) (β-homβ n q p) β©
Ξ½β n - β¦ p β q β§ β Ξ½β n - β¦ q β p β§ β‘Λβ¨ cong (Ξ½β n -_) (cong-proc refl) β¨Ύ Ξ½β-β n _ _ β©
Ξ½β n - β¦ p β₯ q β§ β
step-homβ n a p q with n βββ? a
... | yes nβa =
β¦ Ξ½β n - β¦ a Β· (p β₯ q) β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-β-Β· n a β¦ p β₯ q β§ nβa) β©
β¦ π β§β β‘Λβ¨ Ξ½β-β-Β· n a β¦ p β₯ q β§ nβa β©
Ξ½β n - a Β· β¦ p β₯ q β§ β‘β¨ cong (Ξ½β n -_) (cong-proc refl) β©
Ξ½β n - β.stepβ β¦ a Β· p β§ β¦ q β§ β
... | no nβa =
β¦ Ξ½β n - β¦ a Β· (p β₯ q) β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-β-Β· n a β¦ p β₯ q β§ nβa) β©
β¦ a Β· Ξ½β n - β¦ p β₯ q β§ β§β β‘β¨β©
a Β· β¦ Ξ½β n - β¦ p β₯ q β§ β§β β‘β¨ cong (a Β·_) (β₯-homβ n p q) β©
a Β· Ξ½β n - β¦ p β₯ q β§ β‘Λβ¨ Ξ½β-β-Β· n a β¦ p β₯ q β§ nβa β©
Ξ½β n - a Β· β¦ p β₯ q β§ β‘β¨ cong (Ξ½β n -_) (cong-proc refl) β©
Ξ½β n - β.stepβ β¦ a Β· p β§ β¦ q β§ β
sync-homβ n (inp a) p `π =
π-homβ n _ _ (syncπΚ³ (inp a) p) (cong-proc refl)
sync-homβ n a p (qβ `β qβ) =
β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β qβ β§ β§β β‘β¨ cong (β¦_β§β β Ξ½β n -_) (syncα΅’β-βΚ³ _ _ _ _) β©
β¦ Ξ½β n - (syncα΅’β β¦ a Β· p β§ β¦ qβ β§ β syncα΅’β β¦ a Β· p β§ β¦ qβ β§) β§β β‘β¨ cong β¦_β§β (Ξ½β-β n _ _) β©
β¦ (Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β§) β (Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β§) β§β β‘β¨β©
β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β§ β§β β β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β§ β§β β‘β¨ congβ _β_ (sync-homβ n a p qβ) (sync-homβ n a p qβ) β©
(Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ qβ β§) β (Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ qβ β§) β‘Λβ¨ Ξ½β-β n _ _ β©
Ξ½β n - (β.syncα΅’β β¦ a Β· p β§ β¦ qβ β§ β β.syncα΅’β β¦ a Β· p β§ β¦ qβ β§) β‘Λβ¨ cong (Ξ½β n -_) (β.syncα΅’β-βΚ³ _ _ _) β©
Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ qβ β qβ β§ β
sync-homβ n a p (qβ `β₯ qβ) =
β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β₯ qβ β§ β§β β‘β¨β©
β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β qβ β qβ β qβ β§ β§β β‘β¨ sync-homβ n a p (qβ β qβ β qβ β qβ) β©
Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ qβ β qβ β qβ β qβ β§ β‘β¨ cong (Ξ½β n -_) (cong (β.syncα΅’β β¦ a Β· p β§) (cong-proc refl)) β©
Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ qβ β₯ qβ β§ β
sync-homβ n (out a) p q =
π-homβ n _ _ (sync-out a β¦ p β§ q) (cong-proc refl)
sync-homβ n Ο p q = π-homβ n _ _ (sync-Ο β¦ p β§ q) (cong-proc refl)
sync-homβ n a p (qβ `β qβ) =
β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ qβ β qβ β§ β§β β‘β¨ cong (β¦_β§β β Ξ½β n -_) (syncα΅’β-assoc a β¦ p β§ _ _) β©
β¦ Ξ½β n - syncα΅’β β¦ a Β· (p β₯ qβ) β§ β¦ qβ β§ β§β β‘β¨ sync-homβ n a (p β₯ qβ) qβ β©
Ξ½β n - β.syncα΅’β β¦ a Β· (p β₯ qβ) β§ β¦ qβ β§ β‘β¨ cong (Ξ½β n -_) (β.syncα΅’β-assoc a β¦ p β§ β¦ qβ β§ β¦ qβ β§) β©
Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ qβ β qβ β§ β
sync-homβ ns a p (`Ξ½ n - q) =
let m = # ((a Β· p) β q)
in
β¦ Ξ½β ns - syncα΅’β β¦ a Β· p β§ β¦ Ξ½ n - q β§ β§β
β‘β¨ cong β¦_β§β ( Ξ½-sync-rewrite ns n a p q) β©
β¦ Ξ½β (m β· ns) - syncα΅’β β¦ a Β· p β§ β¦ `Ο (n /β m) q β§ β§β
β‘β¨ sync-homβ (m β· ns) a p (`Ο (n /β m) q) β©
Ξ½β (m β· ns) - β.syncα΅’β β¦ a Β· p β§ β¦ `Ο (n /β m) q β§
β‘Λβ¨ cong (Ξ½β ns -_) (β.Ξ½-sync-rewrite n a p q) β©
Ξ½β ns - β.syncα΅’β β¦ a Β· p β§ β¦ Ξ½ n - q β§ β
sync-homβ n a p (`! q) =
β¦ Ξ½β n - syncα΅’β β¦ a Β· p β§ β¦ ! q β§ β§β
β‘β¨ cong (β¦_β§β β Ξ½β n -_) (cong (syncα΅’β β¦ a Β· p β§) (!-β β¦ q β§) β¨Ύ syncα΅’β-assoc a β¦ p β§ _ _) β©
β¦ Ξ½β n - syncα΅’β β¦ a Β· (p β₯ ! q) β§ β¦ q β§ β§β
β‘β¨ sync-homβ n a (p β₯ ! q) q β©
Ξ½β n - β.syncα΅’β β¦ a Β· (p β₯ ! q) β§ β¦ q β§
β‘β¨ cong (Ξ½β n -_) (β.syncα΅’β-assoc a β¦ p β§ β¦ ! q β§ β¦ q β§ β¨Ύ cong (β.syncα΅’β β¦ a Β· p β§) (sym (!-β β¦ q β§))) β©
Ξ½β n - β.syncα΅’β β¦ a Β· p β§ β¦ ! q β§ β
sync-homβ n (inp a) p (Ο `Β· q) =
π-homβ n _ _ (sync-nomatch (inp a) Ο β¦ p β§ β¦ q β§ Ξ» ()) (cong-proc refl)
sync-homβ n (inp a) p (inp b `Β· q) =
π-homβ n _ _ (sync-nomatch (inp a) (inp b) β¦ p β§ β¦ q β§ Ξ» ()) (cong-proc refl)
sync-homβ n (inp a) p (out b `Β· q) with a β b
... | no aβ’b =
π-homβ n _ _ (sync-nomatch (inp a) (out b) β¦ p β§ β¦ q β§ aβ’b) (β.syncα΅’β-nomatch (inp a) (out b) β¦ p β§ β¦ q β§ aβ’b)
... | yes aβ‘b =
β¦ Ξ½β n - syncα΅’β β¦ inp a Β· p β§ β¦ out b Β· q β§ β§β β‘β¨ cong (β¦_β§β β (Ξ½β n -_)) (sync-match (inp a) (out b) p β¦ q β§ aβ‘b) β©
β¦ Ξ½β n - Ο Β· β¦ p β₯ q β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-β-Β· n Ο β¦ p β₯ q β§ Ξ» ()) β©
Ο Β· β¦ Ξ½β n - β¦ p β₯ q β§ β§β β‘β¨ cong (Ο Β·_) (β₯-homβ n p q) β©
Ο Β· Ξ½β n - β¦ p β₯ q β§ β‘Λβ¨ Ξ½β-β-Β· n Ο β¦ p β₯ q β§ (Ξ» ()) β©
Ξ½β n - Ο Β· β¦ p β₯ q β§ β‘Λβ¨ cong (Ξ½β n -_) (cong-proc (cong (bool β
_) (it-does (a β b) aβ‘b) )) β©
Ξ½β n - β.syncα΅’β β¦ inp a Β· p β§ β¦ out b Β· q β§ β
β-homβ n `π q =
β¦ Ξ½β n - β¦ π β q β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-π n β¦ q β§) β©
π β‘Λβ¨ Ξ½β-π n β¦ q β§ β©
Ξ½β n - β¦ π β q β§ β
β-homβ n (pβ `β pβ) q =
β¦ Ξ½β n - β¦ (pβ β pβ) β q β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-β β¦ pβ β§ β¦ pβ β§ n β¦ q β§) β©
β¦ Ξ½β n - β¦ pβ β q β§ β§β β β¦ Ξ½β n - β¦ pβ β q β§ β§β β‘β¨ congβ _β_ (β-homβ n pβ q) (β-homβ n pβ q) β©
Ξ½β n - β¦ pβ β q β§ β Ξ½β n - β¦ pβ β q β§ β‘Λβ¨ Ξ½β-β β¦ pβ β§ β¦ pβ β§ n β¦ q β§ β©
Ξ½β n - β¦ (pβ β pβ) β q β§ β
β-homβ n (pβ `β pβ) q =
β¦ Ξ½β n - β¦ (pβ β pβ) β q β§ β§β β‘β¨ cong (Ξ» e β β¦ Ξ½β n - e β§β) (β-assoc β¦ pβ β§ β¦ pβ β§ β¦ q β§) β©
β¦ Ξ½β n - β¦ pβ β (pβ β₯ q) β§ β§β β‘β¨ β-homβ n pβ (pβ β₯ q) β©
Ξ½β n - β¦ pβ β (pβ β₯ q) β§ β‘Λβ¨ cong (Ξ½β n -_) (β-assoc β¦ pβ β§ β¦ pβ β§ β¦ q β§) β©
Ξ½β n - β¦ (pβ β pβ) β q β§ β
β-homβ n (pβ `β₯ pβ) q =
β¦ Ξ½β n - β¦ (pβ β₯ pβ) β q β§ β§β β‘β¨ cong (Ξ» e β β¦ Ξ½β n - (e β β¦ q β§) β§β) (β-β₯ β¦ pβ β§ β¦ pβ β§) β©
β¦ Ξ½β n - β¦ (pβ β pβ β pβ β pβ) β q β§ β§β β‘β¨ cong β¦_β§β (Ξ½β-β β¦ pβ β pβ β§ β¦ pβ β pβ β§ n β¦ q β§) β©
β¦ Ξ½β n - β¦ pβ β pβ β q β§ β§β β β¦ Ξ½β n - β¦ pβ β pβ β q β§ β§β β‘β¨ congβ _β_ (cong (β¦_β§β β Ξ½β n -_) (β-assoc β¦ pβ β§ β¦ pβ β§ β¦ q β§)) (cong (β¦_β§β β Ξ½β n -_) (β-assoc β¦ pβ β§ β¦ pβ β§ β¦ q β§)) β©
β¦ Ξ½β n - β¦ pβ β (pβ β₯ q) β§ β§β β β¦ Ξ½β n - β¦ pβ β (pβ β₯ q) β§ β§β β‘β¨ congβ _β_ (β-homβ n pβ (pβ β₯ q)) (β-homβ n pβ (pβ β₯ q)) β©
Ξ½β n - β¦ pβ β (pβ β₯ q) β§ β Ξ½β n - β¦ pβ β (pβ β₯ q) β§ β‘Λβ¨ congβ _β_ (cong (Ξ½β n -_) (β-assoc β¦ pβ β§ β¦ pβ β§ β¦ q β§)) (cong (Ξ½β n -_) (β-assoc β¦ pβ β§ β¦ pβ β§ β¦ q β§)) β©
Ξ½β n - β¦ pβ β pβ β q β§ β Ξ½β n - β¦ pβ β pβ β q β§ β‘Λβ¨ Ξ½β-β β¦ pβ β pβ β§ β¦ pβ β pβ β§ n β¦ q β§ β©
Ξ½β n - ((β¦ pβ β§ β β¦ pβ β§ β β¦ pβ β§ β β¦ pβ β§) β β¦ q β§) β‘Λβ¨ cong (Ξ» e β Ξ½β n - (e β β¦ q β§)) (β-β₯ β¦ pβ β§ β¦ pβ β§) β©
Ξ½β n - (β¦ pβ β§ β₯ β¦ pβ β§ β β¦ q β§) β
β-homβ n (`! p) q =
β¦ Ξ½β n - β¦ ! p β q β§ β§β β‘β¨ cong (Ξ» e β β¦ Ξ½β n - (e β β¦ q β§) β§β) (!-β β¦ p β§) β©
β¦ Ξ½β n - β¦ p β ! p β q β§ β§β β‘β¨ cong (Ξ» e β β¦ Ξ½β n - e β§β) (β-assoc β¦ p β§ β¦ ! p β§ β¦ q β§) β©
β¦ Ξ½β n - β¦ p β (! p β₯ q) β§ β§β β‘β¨ β-homβ n p (! p β₯ q) β©
Ξ½β n - β¦ p β (! p β₯ q) β§ β‘Λβ¨ cong (Ξ½β n -_) (β-assoc β¦ p β§ β¦ ! p β§ β¦ q β§) β©
Ξ½β n - β¦ p β ! p β q β§ β‘Λβ¨ cong (Ξ» e β Ξ½β n - (e β β¦ q β§)) (!-β β¦ p β§) β©
Ξ½β n - β¦ ! p β q β§ β
β-homβ n (a `Β· p) q =
β¦ Ξ½β n - β¦ a Β· p β q β§ β§β
β‘β¨ cong (β¦_β§β β (Ξ½β n -_)) (Β·β-decomp a β¦ p β§ β¦ q β§) β©
β¦ Ξ½β n - (syncα΅’β (a Β· β¦ p β§) β¦ q β§ β stepβ (a Β· β¦ p β§) β¦ q β§) β§β
β‘β¨ cong β¦_β§β (Ξ½β-β n _ _) β©
β¦ Ξ½β n - syncα΅’β (a Β· β¦ p β§) β¦ q β§ β§β β β¦ Ξ½β n - stepβ (a Β· β¦ p β§) β¦ q β§ β§β
β‘β¨ congβ _β_ (sync-homβ n a p q) (cong (β¦_β§β β Ξ½β n -_) (step-Β· a β¦ p β§ β¦ q β§ β¨Ύ cong (a Β·_) (β₯-comm β¦ q β§ β¦ p β§)) β¨Ύ step-homβ n a p q) β©
(Ξ½β n - β.syncα΅’β (a Β· β¦ p β§) β¦ q β§) β (Ξ½β n - β.stepβ (a Β· β¦ p β§) β¦ q β§)
β‘Λβ¨ Ξ½β-β n _ _ β©
Ξ½β n - (β.syncα΅’β (a Β· β¦ p β§) β¦ q β§ β β.stepβ (a Β· β¦ p β§) β¦ q β§)
β‘β¨ cong (Ξ½β n -_) (cong-proc refl) β©
Ξ½β n - β¦ a Β· p β q β§ β
β-homβ ns (`Ξ½ n - p) q =
let m = # (p β q)
in
β¦ Ξ½β ns - β¦ Ξ½ n - p β q β§ β§β
β‘β¨ cong β¦_β§β (Ξ½-β-rewrite ns n p q) β©
β¦ Ξ½β (m β· ns) - β¦ `Ο (n /β m) p β q β§ β§β
β‘β¨ β-homβ (m β· ns) (`Ο (n /β m) p) q β©
Ξ½β (m β· ns) - β¦ `Ο (n /β m) p β q β§
β‘Λβ¨ β.Ξ½-β-rewrite ns n p q β©
Ξ½β ns - β¦ Ξ½ n - p β q β§ β
homβ : β (p : P A) β β¦ β¦ p β§ β§β β‘ β¦ p β§
homβ p =
β¦ β¦ p β§ β§β β‘Λβ¨ cong β¦_β§β (βπ β¦ p β§) β©
β¦ β¦ p β§ β π β§β β‘β¨ β-homβ [] p π β©
β¦ p β π β§ β‘β¨ βπ β¦ p β§ β©
β¦ p β§ β