{-# OPTIONS --sized-types #-}
module Up-to.Closure where
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude as P
open import Prelude.Size
open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)
import Bisimilarity
open import Indexed-container hiding (Bisimilarity)
open import Indexed-container.Combinators hiding (id; _∘_)
open import Labelled-transition-system
import Labelled-transition-system.CCS
open import Relation
import Similarity
import Similarity.CCS as SC
open import Up-to
private
module CCS {ℓ} (Name : Type ℓ) where
open Labelled-transition-system.CCS Name public
open module B = Bisimilarity CCS public
open module S = Similarity CCS public using (Similarity)
Compatible-⊗ :
∀ {ℓ} {I : Type ℓ} {C₁ C₂ : Container I I} {F : Trans ℓ I} →
Monotone F →
Compatible C₁ F → Compatible C₂ F → Compatible (C₁ ⊗ C₂) F
Compatible-⊗ {C₁ = C₁} {C₂} {F} mono comp₁ comp₂ {R = R} =
F (⟦ C₁ ⊗ C₂ ⟧ R) ⊆⟨ mono (⟦⊗⟧↔ _ C₁ C₂) ⟩
F (⟦ C₁ ⟧ R ∩ ⟦ C₂ ⟧ R) ⊆⟨ (λ x → mono proj₁ x , mono proj₂ x) ⟩
F (⟦ C₁ ⟧ R) ∩ F (⟦ C₂ ⟧ R) ⊆⟨ Σ-map comp₁ comp₂ ⟩
⟦ C₁ ⟧ (F R) ∩ ⟦ C₂ ⟧ (F R) ⊆⟨ _⇔_.from (⟦⊗⟧↔ _ C₁ C₂) ⟩∎
⟦ C₁ ⊗ C₂ ⟧ (F R) ∎
Compatible-reindex₁ :
∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
Monotone F → Symmetric f F →
Compatible C F → Compatible (reindex₁ f C) F
Compatible-reindex₁ {C = C} {F} {f} mono hyp comp {R = R} =
F (⟦ reindex₁ f C ⟧ R) ⊆⟨ mono (⟦reindex₁⟧↔ _ C) ⟩
F (⟦ C ⟧ (R ∘ f)) ⊆⟨ comp ⟩
⟦ C ⟧ (F (R ∘ f)) ⊆⟨ map C (hyp _) ⟩
⟦ C ⟧ (F R ∘ f) ⊆⟨ _⇔_.from (⟦reindex₁⟧↔ _ C) ⟩∎
⟦ reindex₁ f C ⟧ (F R) ∎
Compatible-reindex₂ :
∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
Symmetric f F →
Compatible C F → Compatible (reindex₂ f C) F
Compatible-reindex₂ {C = C} {F} {f} hyp comp {R = R} =
F (⟦ reindex₂ f C ⟧ R) ⊆⟨⟩
F (⟦ C ⟧ R ∘ f) ⊆⟨ hyp _ ⟩
F (⟦ C ⟧ R) ∘ f ⊆⟨ comp ⟩
⟦ C ⟧ (F R) ∘ f ⊆⟨ id ⟩∎
⟦ reindex₂ f C ⟧ (F R) ∎
Compatible-reindex :
∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
Monotone F → Symmetric f F →
Compatible C F → Compatible (reindex f C) F
Compatible-reindex {C = C} {F} {f} mono hyp =
Compatible C F ↝⟨ Compatible-reindex₁ mono hyp ⟩
Compatible (reindex₁ f C) F ↝⟨ Compatible-reindex₂ hyp ⟩
Compatible (reindex₂ f (reindex₁ f C)) F ↔⟨⟩
Compatible (reindex f C) F □
Compatible-⟷ :
∀ {ℓ} {I : Type ℓ}
{C₁ C₂ : Container (I × I) (I × I)} {F : Trans₂ ℓ I} →
Monotone F → Symmetric swap F →
Compatible C₁ F → Compatible C₂ F → Compatible (C₁ ⟷ C₂) F
Compatible-⟷ {C₁ = C₁} {C₂} {F} mono sym = curry (
Compatible C₁ F × Compatible C₂ F ↝⟨ Σ-map id (Compatible-reindex mono sym) ⟩
Compatible C₁ F × Compatible (reindex swap C₂) F ↝⟨ uncurry (Compatible-⊗ mono) ⟩
Compatible (C₁ ⊗ reindex swap C₂) F ↔⟨⟩
Compatible (C₁ ⟷ C₂) F □)
compatible-for-similarity→compatible-for-bisimilarity :
∀ {ℓ} {lts : LTS ℓ} {F} →
Monotone F → Symmetric swap F →
Compatible (Similarity.StepC lts) F →
Compatible (Bisimilarity.StepC lts) F
compatible-for-similarity→compatible-for-bisimilarity mono sym comp =
Compatible-⟷ mono sym comp comp
Size-preserving-reindex :
∀ {ℓ} {I : Type ℓ} {C : Container I I} {F : Trans ℓ I} {f : I → I} →
f ∘ f ≡ id → Symmetric f F →
Size-preserving C F → Size-preserving (reindex f C) F
Size-preserving-reindex {C = C} {F} {f}
inv hyp pres {R = R} {i = i} R⊆ =
F R ⊆⟨ (λ {x} → subst (λ g → F (R ∘ g) x) (sym inv)) ⟩
F (R ∘ f ∘ f) ⊆⟨ hyp _ ⟩
F (R ∘ f) ∘ f ⊆⟨ pres (
R ∘ f ⊆⟨ R⊆ ⟩
ν (reindex f C) i ∘ f ⊆⟨ _⇔_.to (ν-reindex⇔ inv) ⟩
ν C i ∘ f ∘ f ⊆⟨ (λ {x} → subst (λ g → ν C i (g x)) inv) ⟩∎
ν C i ∎) ⟩
ν C i ∘ f ⊆⟨ _⇔_.from (ν-reindex⇔ inv) ⟩∎
ν (reindex f C) i ∎
¬-Size-preserving-⟷/⊗ :
∀ {ℓ} →
({Name : Type ℓ} →
let open CCS Name in
Name →
¬ ({F : Trans₂ ℓ (Proc ∞)} →
Monotone F → Symmetric swap F →
Size-preserving S.StepC F →
Size-preserving B.StepC F))
×
¬ (∀ {lts : LTS ℓ} {F} →
Monotone F → Symmetric swap F →
Size-preserving (Similarity.StepC lts) F →
Size-preserving (Bisimilarity.StepC lts) F)
×
¬ ({I : Type ℓ} {C₁ C₂ : Container (I × I) (I × I)}
{F : Trans₂ ℓ I} →
Monotone F → Symmetric swap F →
Size-preserving C₁ F → Size-preserving C₂ F →
Size-preserving (C₁ ⟷ C₂) F)
×
¬ ({I : Type ℓ} {C₁ C₂ : Container I I} {F : Trans ℓ I} →
Monotone F →
Size-preserving C₁ F → Size-preserving C₂ F →
Size-preserving (C₁ ⊗ C₂) F)
¬-Size-preserving-⟷/⊗ {ℓ} =
Lemmas.contradiction₂
, Lemmas.contradiction₃ (lift tt)
, Lemmas.contradiction₄ (lift tt)
, Lemmas.contradiction₅ (lift tt)
where
module Lemmas {Name : Type ℓ} (a : Name) where
open CCS Name public
≤≥≁ = SC.≤≥≁ a
m₁ = proj₁ ≤≥≁
m₂ = proj₁ (proj₂ ≤≥≁)
F : Trans₂ ℓ (Proc ∞)
F R = R ∪ (_≡ (m₁ , m₂)) ∪ (_≡ (m₂ , m₁))
mono : Monotone F
mono R⊆S = ⊎-map R⊆S id
symm : Symmetric swap F
symm R =
F (R ⁻¹) ⊆⟨⟩
R ⁻¹ ∪ (_≡ (m₁ , m₂)) ∪ (_≡ (m₂ , m₁)) ⊆⟨ ⊎-map id P.[ inj₂ ∘ lemma , inj₁ ∘ lemma ] ⟩
R ⁻¹ ∪ (_≡ (m₁ , m₂)) ⁻¹ ∪ (_≡ (m₂ , m₁)) ⁻¹ ⊆⟨ id ⟩∎
F R ⁻¹ ∎
where
lemma : {p₁ p₂ : Proc ∞ × Proc ∞} → p₁ ≡ swap p₂ → swap p₁ ≡ p₂
lemma refl = refl
pres : Size-preserving S.StepC F
pres {R = R} {i = i} R⊆ =
F R ⊆⟨⟩
R ∪ (_≡ (m₁ , m₂)) ∪ (_≡ (m₂ , m₁)) ⊆⟨ [ R⊆ , helper ] ⟩∎
Similarity i ∎
where
helper : ∀ {p} → p ≡ (m₁ , m₂) ⊎ p ≡ (m₂ , m₁) → Similarity i p
helper (inj₁ refl) = proj₁ (proj₂ (proj₂ ≤≥≁))
helper (inj₂ refl) = proj₁ (proj₂ (proj₂ (proj₂ ≤≥≁)))
contradiction =
Size-preserving B.StepC F ↝⟨ (λ hyp → _⇔_.to (monotone→⇔ _ mono) hyp) ⟩
F (Bisimilarity ∞) ⊆ Bisimilarity ∞ ↝⟨ _$ inj₂ (inj₁ refl) ⟩
m₁ ∼ m₂ ↝⟨ proj₂ (proj₂ (proj₂ (proj₂ ≤≥≁))) ⟩□
⊥ □
contradiction₂ =
({F : Trans₂ ℓ (Proc ∞)} →
Monotone F → Symmetric swap F →
Size-preserving S.StepC F →
Size-preserving B.StepC F) ↝⟨ (λ closed → closed mono symm pres) ⟩
Size-preserving B.StepC F ↝⟨ contradiction ⟩□
⊥ □
contradiction₃ =
(∀ {lts : LTS ℓ} {F} →
Monotone F → Symmetric swap F →
Size-preserving (Similarity.StepC lts) F →
Size-preserving (Bisimilarity.StepC lts) F) ↝⟨ (λ closed mono sym pres → closed mono sym pres) ⟩
({F : Trans₂ ℓ (Proc ∞)} →
Monotone F → Symmetric swap F →
Size-preserving S.StepC F →
Size-preserving B.StepC F) ↝⟨ contradiction₂ ⟩□
⊥ □
contradiction₄ =
({I : Type ℓ} {C₁ C₂ : Container (I × I) (I × I)}
{F : Trans₂ ℓ I} →
Monotone F → Symmetric swap F →
Size-preserving C₁ F → Size-preserving C₂ F →
Size-preserving (C₁ ⟷ C₂) F) ↝⟨ (λ closed mono symm pres → closed mono symm pres pres) ⟩
(∀ {lts : LTS ℓ} {F} →
Monotone F → Symmetric swap F →
Size-preserving (Similarity.StepC lts) F →
Size-preserving (Bisimilarity.StepC lts) F) ↝⟨ contradiction₃ ⟩□
⊥ □
contradiction₅ =
({I : Type ℓ} {C₁ C₂ : Container I I}
{F : Trans ℓ I} →
Monotone F →
Size-preserving C₁ F → Size-preserving C₂ F →
Size-preserving (C₁ ⊗ C₂) F) ↝⟨ (λ closed → closed mono pres) ⟩
(Size-preserving (reindex swap S.StepC) F →
Size-preserving B.StepC F) ↝⟨ _$ Size-preserving-reindex refl symm pres ⟩
Size-preserving B.StepC F ↝⟨ contradiction ⟩□
⊥ □