Progress & Preservation for Simply Typed Lambda Calculus

STLC.agda

open import Level using (0ℓ)
open import Data.Nat as N using (ℕ; suc)
open import Data.Vec as Vc using (Vec; []; _∷_)
open import Data.Fin as Fn using (Fin; suc; zero)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Data.Fin.Substitution as Sbt using (Sub)

open import Codata.Thunk using (force)
open import Codata.Delay as Del using (Delay)

module STLC where

infix  4 _↝_ _⟶_ _⟶*_ _⊢_∶_ ∙⊢_∶_ _⊢_⊣_
infix  6 _at_
infixl 7 _$_ _$ˡ_ _$ʳ_
infix  8 _[_] _/_ _/¹_

_at_ : ∀ {ℓ n} {A : Set ℓ} → Vec A n → Fin n → A
v at i = Vc.lookup i v

------------------------------------------------------------------------------------------
-- Semantics

PrimOp = ℕ → ℕ

-- Syntax
data Exp n : Set where
  ⟨⟩ : Exp n                        -- unit
  nat : ℕ → Exp n                  -- number
  δ : PrimOp → Exp n               -- primitive function
  var : (x : Fin n) → Exp n        -- variable
  _$_ : (e e₁ : Exp n) → Exp n     -- application
  ƛ : (e : Exp (suc n)) → Exp n    -- abstraction

-- Values
data Val : Set where
  ⟨⟩ : Val                          -- unit
  nat : ℕ → Val                   -- number
  δ : PrimOp → Val
  ƛ : Exp 1 → Val                  -- lambda function

⌊_⌋ : Val → Exp 0
⌊ ⟨⟩   ⌋ = ⟨⟩
⌊ nat n ⌋ = nat n
⌊ δ f ⌋ = δ f
⌊ ƛ e ⌋ = ƛ e

-- Reduction context (left-to-right eager evaluation)
data Ctx : Set where
  □ : Ctx
  _$ˡ_ : (C : Ctx) (e : Exp 0) → Ctx
  _$ʳ_ : (v : Val) (C : Ctx) → Ctx

_[_] : Ctx → Exp 0 → Exp 0
□         [ e ] = e
(C $ˡ e₁) [ e ] = C [ e ] $ e₁
(v $ʳ C)  [ e ] = ⌊ v ⌋ $ C [ e ]

-- Weakening
punch : ∀ {n} → Fin (suc n) → Exp n → Exp (suc n)
punch y ⟨⟩        = ⟨⟩
punch y (nat c)  = nat c
punch y (δ f)    = δ f
punch y (var x)  = var (Fn.punchIn y x)
punch y (e $ e₁) = punch y e $ punch y e₁
punch y (ƛ e)    = ƛ (punch (suc y) e)

open Sbt.Simple (record
  { var = var
  ; weaken = punch zero })
  using (weaken; _↑; sub)

-- Substitution
_/_ : ∀ {n m} → Exp n → Sub Exp n m → Exp m
⟨⟩        / σ = ⟨⟩
var x    / σ = σ at x
nat c    / σ = nat c
δ f      / σ = δ f
(e $ e₁) / σ = e / σ $ e₁ / σ
ƛ e      / σ = ƛ (e / σ ↑)

_/¹_ : Exp 1 → Val → Exp 0
e /¹ v = e / sub ⌊ v ⌋

-- Reduction rules
data _↝_ : Rel (Exp 0) 0ℓ where
  beta : ∀ {e v}                         -- beta reduction
    → (ƛ e $ ⌊ v ⌋) ↝ (e /¹ v)

  primop : ∀ {c} f                       -- primitive application
    → (δ f $ ⌊ nat c ⌋) ↝ nat (f c)

data _⟶_ : Rel (Exp 0) 0ℓ where
  ctx : ∀ C → _↝_ =[ C [_] ]⇒ _⟶_      -- contextual closure over ↝

data _⟶*_ : Rel (Exp 0) 0ℓ where
  step : _⟶_ ⇒ _⟶*_                   -- reflexive, transitive closure over ⟶
  refl : Reflexive _⟶*_
  trans : Transitive _⟶*_

------------------------------------------------------------------------------------------
-- Types

-- Syntax
data Typ : Set where
  `1 `N : Typ
  _`→_ : (t s : Typ) → Typ

-- Judgments
data _⊢_∶_ {n} Γ : Exp n → Typ → Set where
  ⟨⟩ : Γ ⊢ ⟨⟩ ∶ `1                   -- unit
  nat : ∀ c → Γ ⊢ nat c ∶ `N       -- number
  δ : ∀ f → Γ ⊢ δ f ∶ (`N `→ `N)   -- primitive function

  var : ∀ x                        -- variable
    → Γ ⊢ (var x) ∶ (Γ at x)

  _$_ : ∀ {e₁ e₂ t s}              -- application
    → Γ ⊢ e₁ ∶ (t `→ s)
    → Γ ⊢ e₂ ∶ t
    --------
    → Γ ⊢ (e₁ $ e₂) ∶ s

  ƛ : ∀ {e t s}                    -- abstraction
    → (t ∷ Γ) ⊢ e ∶ s
    --------
    → Γ ⊢ (ƛ e) ∶ (t `→ s)

∙⊢_∶_ = [] ⊢_∶_         -- typing under empty context

------------------------------------------------------------------------------------------
-- Proofs

mutual
  PROGRESS = ∀ {e t}
    → ∙⊢ e ∶ t
    → IsValue e ⊎ Reduces e

  PRESERVATION = ∀ {e e′ t}
    → e ⟶ e′
    → ∙⊢ e  ∶ t
    → ∙⊢ e′ ∶ t

  record Reduces e : Set where
    constructor reduces
    field {e′} : _
          red : e ⟶ e′

  record IsValue e : Set where
    constructor is-val
    field {v} : _
          pf : e ≡ ⌊ v ⌋

-- Helpers for augmenting the context in a ⟶ relation
_$ᶜˡ_ : ∀ {e e′} → (e ⟶ e′) → (e₁ : _) → (e $ e₁ ⟶ e′ $ e₁)
(ctx C s) $ᶜˡ e₁ = ctx (C $ˡ e₁) s

_$ᶜʳ_ : ∀ {e e′} → (v : _) → (e ⟶ e′) → (⌊ v ⌋ $ e ⟶ ⌊ v ⌋ $ e′)
v $ᶜʳ (ctx C s) = ctx (v $ʳ C) s

-- *** Progress lemma *** --
mutual
  progress : PROGRESS
  progress {⟨⟩} _      = inj₁ (is-val P.refl)
  progress {nat c} _  = inj₁ (is-val P.refl)
  progress {δ f} _    = inj₁ (is-val P.refl)
  progress {ƛ e} _    = inj₁ (is-val P.refl)
  progress {var ()} _
  progress (tj $ tj₁) with progress tj
  ... | inj₂ (reduces rr)        = inj₂ (reduces (rr $ᶜˡ _))
  ... | inj₁ (is-val {v} P.refl) = inj₂ ($ʳ-progress _ tj tj₁)

  $ʳ-progress : ∀ v {e₁ t s}
    → ∙⊢ ⌊ v ⌋ ∶ (t `→ s)
    → ∙⊢ e₁ ∶ t
    → Reduces (⌊ v ⌋ $ e₁)
  $ʳ-progress v       tj    tj₁  with progress tj₁
  $ʳ-progress v       tj    tj₁     | inj₂ (reduces rr₁)           = reduces (v $ᶜʳ rr₁)
  $ʳ-progress ⟨⟩       ()    tj₁     | inj₁ (is-val P.refl)         -- can't apply unit
  $ʳ-progress (nat x) ()    tj₁     | inj₁ (is-val P.refl)         -- can't apply nat
  $ʳ-progress (δ f)   (δ _) ()      | inj₁ (is-val {⟨⟩} P.refl)     -- can't apply nat to primop
  $ʳ-progress (δ f)   (δ _) ()      | inj₁ (is-val {δ x} P.refl)   -- can't apply primop to primop
  $ʳ-progress (δ f)   (δ _) ()      | inj₁ (is-val {ƛ x} P.refl)   -- can't apply primop to primop
  $ʳ-progress (δ f)   (δ _) (nat _) | inj₁ (is-val {nat c} P.refl) = reduces (ctx □ (primop f))
  $ʳ-progress (ƛ e)   tj    tj₁     | inj₁ (is-val P.refl)         = reduces (ctx □ beta)

-- Substitution typing invariant
_⊢_⊣_ : ∀ {n m} → Vec Typ n → Sub Exp n m → Vec Typ m → Set
Γ ⊢ σ ⊣ Γ′ = ∀ x → Γ′ ⊢ (σ at x) ∶ (Γ at x)

mutual
  -- Substitution type invariant preserved under weakening (↑)
  ⊢⊣↑ : ∀ {n m} {σ : Sub Exp n m} {Γ Γ′}
    →   Γ   ⊢ σ   ⊣   Γ′
    → ∀ t
    → t ∷ Γ ⊢ σ ↑ ⊣ t ∷ Γ′
  ⊢⊣↑         ψ t zero    = var zero
  ⊢⊣↑ {σ = σ} ψ t (suc i) =
    P.subst (_ ⊢_∶ _)
      (P.sym (lookup-map i weaken σ))  -- (σ ↑) at (suc i) ≡ weaken (σ at i)
      (⊢-punch (ψ i) zero)
    where open import Data.Vec.Properties using (lookup-map)

  ⊢-punch : ∀ {n Γ t} {e : Exp n}
    → Γ ⊢ e ∶ t
    → ∀ y {s}
    → Vc.insert y s Γ ⊢ punch y e ∶ t
  ⊢-punch ⟨⟩          y = ⟨⟩
  ⊢-punch (nat c)    y = nat c
  ⊢-punch (δ f)      y = δ f
  ⊢-punch (tj $ tj₁) y = ⊢-punch tj y $ ⊢-punch tj₁ y
  ⊢-punch (ƛ tj)     y = ƛ (⊢-punch tj (suc y))
  ⊢-punch (var x)    y =
    P.subst (_ ⊢ _ ∶_)
      (insert-punchIn y _ _ x)  -- (insert y s Γ) at (punchIn y x) ≡ Γ at x
      (var (Fn.punchIn y x))
    where open import Data.Vec.Properties using (insert-punchIn)

-- Substitution lemma
substitution : ∀ {n m Γ Γ′} (σ : Sub Exp n m) (ψ : Γ ⊢ σ ⊣ Γ′)
  → ∀ e t
  → Γ  ⊢ e     ∶ t
  → Γ′ ⊢ e / σ ∶ t
substitution σ ψ ⟨⟩        `1       ⟨⟩          = ⟨⟩
substitution σ ψ (nat c)  `N       (nat .c)   = nat c
substitution σ ψ (δ f)    (`N `→ `N) (δ .f)   = δ f
substitution σ ψ (var x)  _        (var .x)   = ψ x
substitution σ ψ (e $ e₁) t        (tj $ tj₁) = substitution σ ψ e _ tj $ substitution σ ψ e₁ _ tj₁
substitution σ ψ (ƛ e)    (t `→ s) (ƛ tj)     = ƛ (substitution (σ ↑) (⊢⊣↑ ψ t) e s tj)

-- Swap the expression in a context as long as types agree
swap-in-ctx : ∀ {e e′}
  → (∀ {s} → ∙⊢ e ∶ s → ∙⊢ e′ ∶ s)
  → ∀ C {t}
  → ∙⊢ C [ e  ] ∶ t
  → ∙⊢ C [ e′ ] ∶ t
swap-in-ctx f □        tj               = f tj
swap-in-ctx f (C $ˡ e) (C[tj] $ C[tj₁]) = swap-in-ctx f C C[tj] $ C[tj₁]
swap-in-ctx f (v $ʳ C) (C[tj] $ C[tj₁]) = C[tj] $ swap-in-ctx f C C[tj₁]

-- *** Preservation lemma *** --
preservation : PRESERVATION
preservation (ctx C stp) C[tj] = swap-in-ctx (pres stp) C C[tj]
  where
  -- Preservation for ↝
  pres : ∀ {e e′ t}
    → e ↝ e′
    → ∙⊢ e  ∶ t
    → ∙⊢ e′ ∶ t

  pres beta (ƛ tj $ tj₁) = substitution (sub _) ψ _ _ tj
    where ψ = λ { zero → tj₁ ; (suc ()) }

  pres (primop f) (δ .f $ tj₁) = nat (f _)

-- Evaluation beginning with "e" halts with a value of type "t"
record ⇓ e t : Set where
  constructor halts
  field {v} : Val
        reduction : e ⟶* ⌊ v ⌋
        typing : ∙⊢ ⌊ v ⌋ ∶ t

mutual
  correct : ∀ {e t} → (∙⊢ e ∶ t) → ∀ {sz} → Delay (⇓ e t) sz
  correct tj with progress tj
  ... | inj₁ (is-val P.refl) =
    Del.now (halts refl tj)
  ... | inj₂ (reduces rr) =
    Del.map (rr ◅_) (Del.later λ where .force → correct (preservation rr tj))

  _◅_ : ∀ {e e′ t} → (e ⟶ e′) → (⇓ e′ t) → (⇓ e t)
  rr ◅ halts rr* tj = halts (trans (step rr) rr*) tj

  eval : ∀ e t → (∙⊢ e ∶ t) → ∀ {sz} → Delay Val sz
  eval _ _ tj = Del.map ⇓.v (correct tj)

add1 : ∀ {n} → Exp n
add1 = δ suc

example : Exp 0
example = ƛ (ƛ (add1 $ var (suc zero))) $ nat 8 $ ⟨⟩   -- (\x.\y.add1 x) 8 ()

ex-eval : eval example `N (ƛ (ƛ (δ suc $ var (suc zero))) $ nat 8 $ ⟨⟩)  -- typechecking proof
            Del.⇓
ex-eval = Del.later (Del.later (Del.later (Del.now _)))

ex-test : Del.extract ex-eval ≡ nat 9
ex-test = P.refl