Normalization by Evaluation for Simply Typed Lambda Calculus

normalize.lean

-- https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
-- http://www.rntz.net/post/2019-01-18-binding-in-agda.html
-- Agda version: https://gist.github.com/pedrominicz/74dfec469ce44ccb88ccf8d04c084727

inductive type : Type
| arrow : type → type → type
| unit : type

def ctx : Type 1 := type → Type

def ctx.nil : ctx := λ A, empty

def ctx.cons (Γ : ctx) (A : type) : ctx :=
λ B, psum (A = B) (Γ B)

inductive term : ctx → type → Type 1
| var {Γ : ctx} {A} : Γ A → term Γ A
| lam {Γ A B} : term (ctx.cons Γ A) B → term Γ (type.arrow A B)
| app {Γ A B} : term Γ (type.arrow A B) → term Γ A → term Γ B

inductive typing : bool → ctx → type → Type 1
| lam {Γ A B} : typing ff (ctx.cons Γ A) B → typing ff Γ (type.arrow A B)
| unit {Γ} : typing tt Γ type.unit → typing ff Γ type.unit
| var {Γ : ctx} {A} : Γ A → typing tt Γ A
| app {Γ A B} : typing tt Γ (type.arrow A B) → typing ff Γ A → typing tt Γ B

def ctx.subset (Γ Δ : ctx) : Type := Π A, Γ A → Δ A

def ctx.ext {Γ Δ A} (ρ : ctx.subset Γ Δ) : ctx.subset (ctx.cons Γ A) (ctx.cons Δ A)
| A (psum.inl rfl) := psum.inl rfl
| A (psum.inr x)   := psum.inr (ρ A x)

set_option eqn_compiler.lemmas false

def typing.rename : Π {Γ Δ A b}, ctx.subset Γ Δ → typing b Γ A → typing b Δ A
| Γ Δ A ff ρ (typing.lam M)   := typing.lam (typing.rename (ctx.ext ρ) M)
| Γ Δ A ff ρ (typing.unit M)  := typing.unit (typing.rename ρ M)
| Γ Δ A tt ρ (typing.var x)   := typing.var (ρ A x)
| Γ Δ A tt ρ (typing.app M N) := typing.app (typing.rename ρ M) (typing.rename ρ N)

set_option eqn_compiler.lemmas true

def entail : ctx → type → Type 1
| Γ (type.arrow A B) := Π {Δ}, ctx.subset Γ Δ → entail Δ A → entail Δ B
| Γ type.unit        := typing tt Γ type.unit

def motive (Γ A) : bool → Type 1
| ff := entail Γ A → typing ff Γ A
| tt := typing tt Γ A → entail Γ A

def ctx.zero {Γ A} : ctx.cons Γ A A := psum.inl rfl
def ctx.succ {Γ : ctx} : Π A B, Γ B → ctx.cons Γ A B := λ A B, psum.inr

def entail.rebuild : Π {Γ A} b, motive Γ A b
| Γ (type.arrow A B) ff := λ M, typing.lam (entail.rebuild ff (M (ctx.succ A) (entail.rebuild tt (typing.var ctx.zero))))
| Γ type.unit        ff := λ M, typing.unit M
| Γ (type.arrow A B) tt := λ M Δ ρ N, entail.rebuild tt (typing.app (typing.rename ρ M) (entail.rebuild ff N))
| Γ type.unit        tt := λ M, M

def rename {Γ Δ} : ctx.subset Γ Δ → Π {A}, entail Γ A → entail Δ A
| ρ (type.arrow A B) M := λ Ε σ, M (λ A, σ A ∘ ρ A)
| ρ type.unit        M := typing.rename ρ M

def ctx.entail (Γ Δ : ctx) : Type 1 := Π A, Δ A → entail Γ A

def extend {Γ Δ A} (ρ : ctx.entail Γ Δ) (M : entail Γ A) : ctx.entail Γ (ctx.cons Δ A)
| B (psum.inl rfl) := M
| B (psum.inr x)   := ρ B x

def ctx.entail.id {Γ : ctx} : ctx.entail Γ Γ
| A x := entail.rebuild tt (typing.var x)

set_option eqn_compiler.lemmas false

def denotation : Π {Γ Δ A}, ctx.entail Δ Γ → term Γ A → entail Δ A
| Γ Δ A ρ (term.var x)   := ρ A x
| Γ Δ A ρ (term.lam M)   := λ Δ σ x, denotation (@extend Δ Γ _ (λ A, rename σ ∘ ρ A) x) M
| Γ Δ A ρ (term.app M N) := denotation ρ M (λ A, id) (denotation ρ N)

set_option eqn_compiler.lemmas true

def normalize {Γ A} (M : term Γ A) : typing ff Γ A :=
entail.rebuild ff (denotation ctx.entail.id M)