{-# 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ˡ)