Programming Language Foundations in Agda: Bisimulation

Bisimulation.agda

module Bisimulation where

open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Binary.PropositionalEquality
    using (_≡_; refl; cong; cong₂)

-- https://gist.github.com/pedrominicz/155a701293202ddfa56dd6ec02f3af1b
open import More

infix 4 _~_

data _~_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
    ` : ∀ {Γ A} (x : A ∈ Γ)
        -----------
        → ` x ~ ` x

    ƛ : ∀ {Γ A B} {M M† : Γ , A ⊢ B}
        → M ~ M†
        ------------
        → ƛ M ~ ƛ M†

    _·_ : ∀ {Γ A B} {M M† : Γ ⊢ A ⇒ B} {N N† : Γ ⊢ A}
        → M ~ M†
        → N ~ N†
        -----------------
        → M · N ~ M† · N†

    `let : ∀ {Γ A B} {M M† : Γ ⊢ A} {N N† : Γ , A ⊢ B}
        → M ~ M†
        → N ~ N†
        ------------------------
        → `let M N ~ (ƛ N†) · M†

    `tt : ∀ {Γ}
        ---------------
        → `tt ~ `tt {Γ}

_† : ∀ {Γ A}
    → Γ ⊢ A
    -------
    → Γ ⊢ A
` x †      = ` x
ƛ M †      = ƛ (M †)
(M · N) †  = (M †) · (N †)
`let M N † = (ƛ (N †)) · (M †)
`tt †      = `tt

†~ : ∀ {Γ A} (M : Γ ⊢ A) {N : Γ ⊢ A}
    → M † ≡ N
    ---------
    → M ~ N
†~ (` x)      refl = ` x
†~ (ƛ M)      refl = ƛ (†~ M refl)
†~ (M · N)    refl = †~ M refl · †~ N refl
†~ (`let M N) refl = `let (†~ M refl) (†~ N refl)
†~ `tt        refl = `tt

~† : ∀ {Γ A} {M N : Γ ⊢ A}
    → M ~ N
    ---------
    → M † ≡ N
~† (` x)   = refl
~† (ƛ M)   = cong ƛ (~† M)
~† (M · N) = cong₂ _·_ (~† M) (~† N)
~† (`let M N)
    rewrite ~† M | ~† N = refl
~† `tt = refl

~Value : ∀ {Γ A} {M M† : Γ ⊢ A}
    → M ~ M†
    → Value M
    ----------
    → Value M†
~Value (ƛ M) ƛ = ƛ
~Value `tt `tt = `tt

Value~ : ∀ {Γ A} {M M† : Γ ⊢ A}
    → M ~ M†
    → Value M†
    ----------
    → Value M
Value~ (ƛ M) ƛ = ƛ
Value~ `tt `tt = `tt

~rename : ∀ {Γ Δ A} {M M† : Γ ⊢ A}
    → (ρ : Γ ⊆ Δ)
    → M ~ M†
    --------------------------
    → rename ρ M ~ rename ρ M†
~rename ρ (` x)      = ` (ρ x)
~rename ρ (ƛ M)      = ƛ (~rename (ext ρ) M)
~rename ρ (M · N)    = ~rename ρ M · ~rename ρ N
~rename ρ (`let M N) = `let (~rename ρ M) (~rename (ext ρ) N)
~rename ρ `tt        = `tt

~exts : ∀ {Γ Δ}
    → {σ  : Γ ⊑ Δ}
    → {σ† : Γ ⊑ Δ}
    → (∀ {A}   (x : A ∈ Γ)     → σ x ~ σ† x)
    ----------------------------------------------------
    → (∀ {A B} (x : A ∈ Γ , B) → exts σ x ~ exts σ† x)
~exts σ zero    = ` zero
~exts σ (suc x) = ~rename suc (σ x)

~subst : ∀ {Γ Δ}
    → {σ  : Γ ⊑ Δ}
    → {σ† : Γ ⊑ Δ}
    → (∀ {A} (x : A ∈ Γ) → σ x ~ σ† x)
    -----------------------------------------------------------
    → (∀ {A} {M M† : Γ ⊢ A} → M ~ M† → subst σ M ~ subst σ† M†)
~subst σ (` x)      = σ x
~subst σ (ƛ M)      = ƛ (~subst (~exts σ) M)
~subst σ (M · N)    = ~subst σ M · ~subst σ N
~subst σ (`let M N) = `let (~subst σ M) (~subst (~exts σ) N)
~subst σ `tt        = `tt

_~[_] : ∀ {Γ A B} {M M† : Γ , A ⊢ B} {N N† : Γ ⊢ A}
    → M ~ M†
    → N ~ N†
    ---------------------
    → M [ N ] ~ M† [ N† ]
_~[_] {Γ} {A} M N = ~subst σ M
    where
    σ : ∀ {B} (x : B ∈ Γ , A) → _ ~ _
    σ zero    = N
    σ (suc x) = ` x

-- M  —— —→ —— N
-- |           |
-- |           |
-- ~           ~
-- |           |
-- |           |
-- M† —— —→ —— N†

pattern leg M M†—→N† = ⟨ _ , ⟨ M , M†—→N† ⟩ ⟩

sim : ∀ {Γ A} {M M† N : Γ ⊢ A}
    → M ~ M†
    → M —→ N
    -----------------------------
    → ∃[ N† ] (N ~ N† × M† —→ N†)
sim (M · N) (ξ-·₁ M—→M')
    with sim M M—→M'
... | leg M' M†—→M'†       = leg (M' · N)    (ξ-·₁ M†—→M'†)
sim (V · M) (ξ-·₂ VV M—→M')
    with sim M M—→M'
... | leg M' M†—→M'†       = leg (V · M')    (ξ-·₂ (~Value V VV) M†—→M'†)
sim ((ƛ M) · V) (β-ƛ VV)   = leg (M ~[ V ])  (β-ƛ (~Value V VV))
sim (`let M N) (ξ-`let M—→M')
    with sim M M—→M'
... | leg M' M†—→M'†       = leg (`let M' N) (ξ-·₂ ƛ M†—→M'†)
sim (`let V M) (β-`let VV) = leg (M ~[ V ])  (β-ƛ (~Value V VV))