Programming Language Foundations in Agda: Properties

Properties.agda

module Properties where

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_≃_; extensionality)

-- https://gist.github.com/pedrominicz/85144d398289aa112b994214bcbf204e
open import Lambda

V¬—→ : ∀ {M N}
    → Value M
    ------------
    → ¬ (M —→ N)
V¬—→ V-ƛ       ()
V¬—→ V-zero    ()
V¬—→ (V-suc M) (ξ-suc M—→N) = V¬—→ M M—→N

—→¬V : ∀ {M N}
    → M —→ N
    -----------
    → ¬ Value M
—→¬V M—→N M = V¬—→ M M—→N

infix 4 Canonical_⦂_

data Canonical_⦂_ : Term → Type → Set where
    C-ƛ : ∀ {x N A B}
        → ∅ , x ⦂ A ⊢ N ⦂ B
        -------------------------------
        → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)

    C-zero :
        --------------------
        Canonical `zero ⦂ `ℕ

    C-suc : ∀ {V}
        → Canonical V ⦂ `ℕ
        -----------------------
        → Canonical `suc V ⦂ `ℕ

canonical : ∀ {V A}
    → ∅ ⊢ V ⦂ A
    → Value V
    -----------------
    → Canonical V ⦂ A
canonical (⊢ƛ N)   V-ƛ        = C-ƛ N
canonical ⊢zero    V-zero     = C-zero
canonical (⊢suc V) (V-suc V') = C-suc (canonical V V')

value : ∀ {M A}
    → Canonical M ⦂ A
    -----------------
    → Value M
value (C-ƛ N)   = V-ƛ
value C-zero    = V-zero
value (C-suc M) = V-suc (value M)

typed : ∀ {M A}
    → Canonical M ⦂ A
    -----------------
    → ∅ ⊢ M ⦂ A
typed (C-ƛ N)   = ⊢ƛ N
typed C-zero    = ⊢zero
typed (C-suc M) = ⊢suc (typed M)

data Progress (M : Term) : Set where
    step : ∀ {N}
        → M —→ N
        ------------
        → Progress M

    done :
        Value M
        ------------
        → Progress M

progress : ∀ {M A}
    → ∅ ⊢ M ⦂ A
    ------------
    → Progress M
progress (⊢ƛ N) = done V-ƛ
progress (⊢L · ⊢M)
    with progress ⊢L
...    | step L—→L' = step (ξ-·₁ L—→L')
...    | done VL with progress ⊢M
...                 | step M—→M' = step (ξ-·₂ VL M—→M')
...                 | done VM with canonical ⊢L VL
...                              | C-ƛ _ = step (β-ƛ VM)
progress ⊢zero = done V-zero
progress (⊢suc ⊢M) with progress ⊢M
...                   | step M—→M' = step (ξ-suc M—→M')
...                   | done VM    = done (V-suc VM)
progress (⊢case ⊢L ⊢M ⊢N)
    with progress ⊢L
...    | step L—→L' = step (ξ-case L—→L')
...    | done VL with canonical ⊢L VL
...                 | C-zero   = step β-zero
...                 | C-suc CL = step (β-suc (value CL))
progress (⊢μ ⊢M) = step β-μ

Progress-≃ : ∀ {M} → Progress M ≃ Value M ⊎ ∃[ N ](M —→ N)
Progress-≃ {M} = record
    { to      = to
    ; from    = from
    ; from∘to = from∘to
    ; to∘from = to∘from
    }
    where
    to : Progress M → Value M ⊎ ∃[ N ](M —→ N)
    to (step {N} M—→N) = inj₂ (N , M—→N)
    to (done VM)       = inj₁ VM

    from : Value M ⊎ ∃[ N ](M —→ N) → Progress M
    from (inj₁ VM)         = done VM
    from (inj₂ (N , M—→N)) = step M—→N

    from∘to : ∀ (x : Progress M) → from (to x) ≡ x
    from∘to (step {N} M—→N) = refl
    from∘to (done VM)       = refl

    to∘from : ∀  (x : Value M ⊎ ∃[ N ](M —→ N)) → to (from x) ≡ x
    to∘from (inj₁ VM)         = refl
    to∘from (inj₂ (N , M—→N)) = refl

progress' : ∀ {M A}
    → ∅ ⊢ M ⦂ A
    ------------
    → Value M ⊎ ∃[ N ](M —→ N)
progress' (⊢ƛ N) = inj₁ V-ƛ
progress' (_·_ {M = M} {N = N} ⊢L ⊢M)
    with progress' ⊢L
...    | inj₂ (L' , L—→L') = inj₂ (L' · N , ξ-·₁ L—→L')
...    | inj₁ VL with progress' ⊢M
...                 | inj₂ (M' , M—→M') = inj₂ (M · M' , ξ-·₂ VL M—→M')
...                 | inj₁ VM with canonical ⊢L VL
...                              | C-ƛ {x} {M'} _ = inj₂ (M' [ x := N ] , β-ƛ VM)
progress' ⊢zero = inj₁ V-zero
progress' (⊢suc ⊢M) with progress' ⊢M
...                   | inj₂ (M' , M—→M') = inj₂ (`suc M' , ξ-suc M—→M')
...                   | inj₁ VM           = inj₁ (V-suc VM)
progress' (⊢case {x = x} {L = L} {M = M} {N = N} ⊢L ⊢M ⊢N)
    with progress' ⊢L
...    | inj₂ (L' , L—→L') = inj₂ (case L' [zero⇒ M |suc x ⇒ N ] , ξ-case L—→L')
...    | inj₁ VL with canonical ⊢L VL | VL
...                 | C-zero          | _           = inj₂ (M , β-zero)
...                 | C-suc CL        | V-suc {V} _ = inj₂ (N [ x := V ] , β-suc (value CL))
progress' (⊢μ {x = x} {M = M} ⊢M) = inj₂ (M [ x := μ x ⇒ M ] , β-μ)

Value? : ∀ {M A} → ∅ ⊢ M ⦂ A → Dec (Value M)
Value? (⊢ƛ ⊢N)   = yes V-ƛ
Value? (⊢L · ⊢M) = no λ ()
Value? ⊢zero     = yes V-zero
Value? (⊢suc ⊢M) with Value? ⊢M
...                 | yes VM = yes (V-suc VM)
...                 | no ¬VM = no λ { (V-suc VM) → ¬VM VM }
Value? (⊢case ⊢L ⊢M ⊢N) = no λ ()
Value? (⊢μ ⊢M)          = no λ ()

infix 4 _⊆_

_⊆_ : Context → Context → Set
Γ ⊆ Δ = ∀ {x A} → x ⦂ A ∈ Γ → x ⦂ A ∈ Δ

ext : ∀ {Γ Δ x A}
    → Γ ⊆ Δ
    -----------------------
    → Γ , x ⦂ A ⊆ Δ , x ⦂ A
ext ρ Z          = Z
ext ρ (S x≢y ∈x) = S x≢y (ρ ∈x)

rename : ∀ {Γ Δ}
    → (∀ {x A} → x ⦂ A ∈ Γ → x ⦂ A ∈ Δ)
    -----------------------------------
    → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename ρ (⊢` ∈w)          = ⊢` (ρ ∈w)
rename ρ (⊢ƛ ⊢N)          = ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢L · ⊢M)        = (rename ρ ⊢L) · (rename ρ ⊢M)
rename ρ ⊢zero            = ⊢zero
rename ρ (⊢suc ⊢M)        = ⊢suc (rename ρ ⊢M)
rename ρ (⊢case ⊢L ⊢M ⊢N) = ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N)
rename ρ (⊢μ ⊢M)          = ⊢μ (rename (ext ρ) ⊢M)

weaken : ∀ {Γ M A}
    → ∅ ⊢ M ⦂ A
    -----------
    → Γ ⊢ M ⦂ A
weaken {Γ} ⊢M = rename ρ ⊢M
    where
    ρ : ∀ {x A}
        → x ⦂ A ∈ ∅
        -----------
        → x ⦂ A ∈ Γ
    ρ ()

drop : ∀ {Γ x M A B C}
    → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C
    ---------------------------
    → Γ , x ⦂ B ⊢ M ⦂ C
drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
    where
    ρ : ∀ {y C}
        → y ⦂ C ∈ Γ , x ⦂ A , x ⦂ B
        ---------------------------
        → y ⦂ C ∈ Γ , x ⦂ B
    ρ Z                = Z
    ρ (S x≢x Z)        = ⊥-elim (x≢x refl)
    ρ (S y≢x (S _ ∈y)) = S y≢x ∈y

swap : ∀ {Γ x y M A B C}
    → x ≢ y
    → Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C
    ---------------------------
    → Γ , x ⦂ A , y ⦂ B ⊢ M ⦂ C
swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
    where
    ρ : ∀ {z C}
        → z ⦂ C ∈ Γ , y ⦂ B , x ⦂ A
        ---------------------------
        → z ⦂ C ∈ Γ , x ⦂ A , y ⦂ B
    ρ Z                  = S x≢y Z
    ρ (S y≢x Z)          = Z
    ρ (S z≢x (S z≢y ∈z)) = S z≢y (S z≢x ∈z)

subst : ∀ {Γ x N V A B}
    → ∅ ⊢ V ⦂ A
    → Γ , x ⦂ A ⊢ N ⦂ B
    ----------------------
    → Γ ⊢ N [ x := V ] ⦂ B
subst {x = y} ⊢V (⊢` {x = x} Z)
    with x ≟ y
...    | yes _  = weaken ⊢V
...    | no x≢y = ⊥-elim (x≢y refl)
subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∈x))
    with x ≟ y
...    | yes refl = ⊥-elim (x≢y refl)
...    | no _     = ⊢` ∈x
subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N)
    with x ≟ y
...    | yes refl = ⊢ƛ (drop ⊢N)
...    | no x≢y   = ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
subst ⊢V (⊢L · ⊢M) = (subst ⊢V ⊢L) · (subst ⊢V ⊢M)
subst ⊢V ⊢zero     = ⊢zero
subst ⊢V (⊢suc ⊢M) = ⊢suc (subst ⊢V ⊢M)
subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N)
    with x ≟ y
...    | yes refl = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N)
...    | no x≢y   = ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N))
subst {x = y} ⊢V (⊢μ {x = x} ⊢M)
    with x ≟ y
...    | yes refl = ⊢μ (drop ⊢M)
...    | no x≢y   = ⊢μ (subst ⊢V (swap x≢y ⊢M))

preserve : ∀ {M N A}
    → ∅ ⊢ M ⦂ A
    → M —→ N
    -----------
    → ∅ ⊢ N ⦂ A
preserve (⊢L · ⊢M)               (ξ-·₁ L—→L')    = (preserve ⊢L L—→L') · ⊢M
preserve (⊢L · ⊢M)               (ξ-·₂ VL M—→M') = ⊢L · (preserve ⊢M M—→M')
preserve ((⊢ƛ ⊢N) · ⊢V)          (β-ƛ VV)        = subst ⊢V ⊢N
preserve (⊢suc ⊢M)               (ξ-suc M—→M')   = ⊢suc (preserve ⊢M M—→M')
preserve (⊢case ⊢L ⊢M ⊢N)        (ξ-case L—→L')  = ⊢case (preserve ⊢L L—→L') ⊢M ⊢N
preserve (⊢case ⊢L ⊢M ⊢N)        β-zero          = ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV)      = subst ⊢V ⊢N
preserve (⊢μ ⊢M)                 β-μ             = subst (⊢μ ⊢M) ⊢M

data Gas : Set where
    gas : ℕ → Gas

data Finished (N : Term) : Set where
    done : Value N → Finished N
    out-of-gas : Finished N

data Steps (L : Term) : Set where
    steps : ∀ {N} → L —→→ N → Finished N → Steps L

eval : ∀ {L A} → Gas → ∅ ⊢ L ⦂ A → Steps L
eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas
eval {L} (gas (suc n)) ⊢L
    with progress ⊢L
...    | done VL = steps (L ∎) (done VL)
...    | step L—→M with eval (gas n) (preserve ⊢L L—→M)
...                   | steps M—→→N fin = steps (L —→⟨ L—→M ⟩ M—→→N) fin

Normal : Term → Set
Normal M = ∀ {N} → ¬ (M —→ N)

Stuck : Term → Set
Stuck M = Normal M × ¬ Value M

cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E)
    → ∀ {a a' : A} {b b' : B} {c c' : C} {d d' : D}
    → a ≡ a' → b ≡ b' → c ≡ c' → d ≡ d' → f a b c d ≡ f a' b' c' d'
cong₄ f refl refl refl refl = refl

det : ∀ {M M' M''}
    → M —→ M'
    → M —→ M''
    ----------
    → M' ≡ M''
det (ξ-·₁ L—→L')   (ξ-·₁ L—→L'')   = cong₂ _·_ (det L—→L' L—→L'') refl
det (ξ-·₁ L—→L')   (ξ-·₂ VL _)     = ⊥-elim (V¬—→ VL L—→L')
det (ξ-·₂ VL _)    (ξ-·₁ L—→L'')   = ⊥-elim (V¬—→ VL L—→L'')
det (ξ-·₂ _ M—→M') (ξ-·₂ _ M—→M'') = cong₂ _·_ refl (det M—→M' M—→M'')
det (ξ-·₂ _ M—→M') (β-ƛ VM)        = ⊥-elim (V¬—→ VM M—→M')
det (β-ƛ VM)       (ξ-·₂ _ M—→M'') = ⊥-elim (V¬—→ VM M—→M'')
det (β-ƛ _)        (β-ƛ _)         = refl
det (ξ-suc M—→M')  (ξ-suc M—→M'')  = cong `suc_ (det M—→M' M—→M'')
det (ξ-case L—→L') (ξ-case L—→L'') = cong₄ case_[zero⇒_|suc_⇒_] (det L—→L' L—→L'') refl refl refl
det (ξ-case L—→L') β-zero          = ⊥-elim (V¬—→ V-zero L—→L')
det (ξ-case L—→L') (β-suc VL)      = ⊥-elim (V¬—→ (V-suc VL) L—→L')
det β-zero         (ξ-case M—→M'') = ⊥-elim (V¬—→ V-zero M—→M'')
det β-zero         β-zero          = refl
det (β-suc VL)     (ξ-case L—→L'') = ⊥-elim (V¬—→ (V-suc VL) L—→L'')
det (β-suc _)      (β-suc _)       = refl
det β-μ            β-μ             = refl