1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
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ˡ)
|
