Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 87 insertions, 0 deletions

diff --git a/src/Problem22.agda b/src/Problem22.agda
new file mode 100644
index 0000000..a4befd8
--- /dev/null
+++ b/src/Problem22.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --safe #-}
+
+module Problem22
+    (Act : Set)
+    (State : Set)
+    (_─⟨_⟩→_ : State → Act → State → Set) where
+
+open import Data.Empty
+open import Data.Product
+open import Data.Unit
+open import Function.Base using (_∘′_)
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+variable ℓ : Level
+variable α β γ : Act
+variable x x′ y y′ z : State
+
+record Bisimulation(R : State → State → Set ℓ) : Set ℓ where
+  constructor B
+  field
+    left  : R x y → x ─⟨ α ⟩→ x′ → ∃[ y′ ] (y ─⟨ α ⟩→ y′ × R x′ y′)
+    right : R x y → y ─⟨ α ⟩→ y′ → ∃[ x′ ] (x ─⟨ α ⟩→ x′ × R x′ y′)
+
+open Bisimulation
+
+_≈_ : State → State → Set₁
+x ≈ y = ∃[ R ] (Bisimulation R × R x y)
+
+reflexive : x ≈ x
+reflexive .proj₁ = _≡_
+reflexive .proj₂ .proj₁ .left  refl step = _ , step , refl
+reflexive .proj₂ .proj₁ .right refl step = _ , step , refl
+reflexive .proj₂ .proj₂ = refl
+
+symmetric : x ≈ y → y ≈ x
+symmetric x≈y .proj₁ x y = x≈y .proj₁ y x
+symmetric x≈y .proj₂ .proj₁ .left  = x≈y .proj₂ .proj₁ .right
+symmetric x≈y .proj₂ .proj₁ .right = x≈y .proj₂ .proj₁ .left
+symmetric x≈y .proj₂ .proj₂ = x≈y .proj₂ .proj₂
+
+transitive : x ≈ y → y ≈ z → x ≈ z
+transitive x≈y y≈z .proj₁ x z = ∃[ y ] x≈y .proj₁ x y × y≈z .proj₁ y z
+transitive x≈y y≈z .proj₂ .proj₁ .left  (_ , rel₁ , rel₂) stepˡ =
+  let _ , stepᵐ , rel₁′ = x≈y .proj₂ .proj₁ .left rel₁ stepˡ in
+  let _ , stepʳ , rel₂′ = y≈z .proj₂ .proj₁ .left rel₂ stepᵐ in
+  _ , stepʳ , _ , rel₁′ , rel₂′
+transitive x≈y y≈z .proj₂ .proj₁ .right (_ , rel₁ , rel₂) stepʳ =
+  let _ , stepᵐ , rel₂′ = y≈z .proj₂ .proj₁ .right rel₂ stepʳ in
+  let _ , stepˡ , rel₁′ = x≈y .proj₂ .proj₁ .right rel₁ stepᵐ in
+  _ , stepˡ , _ , rel₁′ , rel₂′
+transitive x≈y y≈z .proj₂ .proj₂ = _ , x≈y .proj₂ .proj₂ , y≈z .proj₂ .proj₂
+
+bisim-is-bisim : Bisimulation _≈_
+bisim-is-bisim .left (R , bisim , x≈y) stepˡ =
+  let (y′ , stepʳ , x′≈y′) = bisim .left x≈y stepˡ in
+  y′ , stepʳ , R , bisim , x′≈y′
+bisim-is-bisim .right (R , bisim , x≈y) stepʳ =
+  let (x′ , stepˡ , x′≈y′) = bisim .right x≈y stepʳ in
+  x′ , stepˡ , R , bisim , x′≈y′
+
+data HML : Set where
+    ⟪_⟫_ : Act → HML → HML
+    ⟦_⟧_ : Act → HML → HML
+    _∧_  : HML → HML → HML
+    ⊤′  : HML
+    ¬′_  : HML → HML
+
+variable ϕ ψ : HML
+infixl 10 _⊧_
+_⊧_ : State → HML → Set
+σ ⊧ ⊤′ = ⊤
+σ ⊧ ¬′ ϕ = σ ⊧ ϕ → ⊥
+σ ⊧ ϕ ∧ ψ = (σ ⊧ ϕ) × (σ ⊧ ψ)
+σ ⊧ ⟪ α ⟫ ϕ = ∃[ σ′ ] σ ─⟨ α ⟩→ σ′ × σ′ ⊧ ϕ
+σ ⊧ ⟦ α ⟧ ϕ = ∀ σ′ → σ ─⟨ α ⟩→ σ′ → σ′ ⊧ ϕ
+
+hml-bisim : ∀ ϕ → x ≈ y → x ⊧ ϕ → y ⊧ ϕ
+hml-bisim ⊤′        (R , bisim , x≈y) prf = prf
+hml-bisim (¬′ ϕ)    (R , bisim , x≈y) prf = prf ∘′ hml-bisim ϕ (symmetric (R , bisim , x≈y))
+hml-bisim (ϕ ∧ ψ)   (R , bisim , x≈y) (prf , prf₁) = hml-bisim ϕ (R , bisim , x≈y) prf , hml-bisim ψ (R , bisim , x≈y) prf₁
+hml-bisim (⟪ a ⟫ ϕ) (R , bisim , x≈y) (x′ , stepˡ , prf) =
+  let (y′ , stepʳ , x′≈y′) = bisim .left x≈y stepˡ in
+  y′ , stepʳ , hml-bisim ϕ (R , bisim , x′≈y′) prf
+hml-bisim (⟦ a ⟧ ϕ) (R , bisim , x≈y) prf y′ stepʳ =
+  let (x′ , stepˡ , x′≈y′) = bisim .right x≈y stepʳ in
+  hml-bisim ϕ (R , bisim , x′≈y′) (prf x′ stepˡ)