6. Progress and Preservation
The best way to understand type theory is to implement it!
One promise remains, the one chapter 0 has been advertising since the LawfulMonad aside: something will be proved about the object language, and the theorem will be a type, the proof a program. The language is fully in place, hand-parsed in chapter 1, checked in chapter 2, adjudicated by Lean in chapter 4, and resident since chapter 5; what is missing is a guarantee that its typing discipline means something. This chapter proves type safety twice, once by induction and once by construction.
Metatheory, by induction
Finally, the proofs. Type safety is classically two theorems about an untyped syntax: progress, a closed well-typed term is a value or can take a step, and preservation, a step does not change the type. The Properties chapter of PLFA, under Further reading, walks the pair in Agda, and this section walks them in Lean, over the simply typed fragment of the object language, arrow and unit. The syntax is chapter 2's nameless representation stripped to the fragment; the typing judgment is an inductive proposition, one constructor per rule, with the variable rule reading the context by plain list lookup:
inductive Exp where
| var (i : Nat)
| unit
| lam (body : Exp)
| app (fn arg : Exp)
deriving Reprinductive HasType : List Ty -> Exp -> Ty -> Prop where
| var {ctx i ty} (h : ctx[i]? = some ty) : HasType ctx (.var i) ty
| unit {ctx} : HasType ctx .unit .unit
| lam {ctx dom cod body} (h : HasType (dom :: ctx) body cod) :
HasType ctx (.lam body) (.arrow dom cod)
| app {ctx dom cod fn arg}
(hf : HasType ctx fn (.arrow dom cod)) (ha : HasType ctx arg dom) :
HasType ctx (.app fn arg) codThe operation chapter 2 dodged must now be written down. Normalization by evaluation never substitutes, closures and environments carry that work; small-step reduction substitutes in the open, so the de Bruijn bookkeeping arrives: a shift renumbering free variables past a cutoff, and substitution itself, shifting what it carries as it descends under binders:
/-- Renumber free variables at or above the cutoff `c` by `d`, so a term valid
in one context stays valid when `d` extra binders are inserted at depth `c`. -/
def shift (c d : Nat) : Exp -> Exp
| .var i => if i < c then .var i else .var (i + d)
| .unit => .unit
| .lam body => .lam (shift (c + 1) d body)
| .app fn arg => .app (shift c d fn) (shift c d arg)
/-- Substitute `s` for the variable at index `j`, dropping that binder: indices
above `j` slide down by one, and `s` is shifted as it descends under binders. -/
def subst (j : Nat) (s : Exp) : Exp -> Exp
| .var i => if i < j then .var i else if i = j then s else .var (i - 1)
| .unit => .unit
| .lam body => .lam (subst (j + 1) (shift 0 1 s) body)
| .app fn arg => .app (subst j s fn) (subst j s arg)A value is an introduction form, and reduction is call by value in three rules: the function position first, then the argument, then the beta step, which is one call to subst:
inductive Value : Exp -> Prop where
| unit : Value .unit
| lam {body} : Value (.lam body)
inductive Step : Exp -> Exp -> Prop where
| appL {fn fn' arg} (h : Step fn fn') : Step (.app fn arg) (.app fn' arg)
| appR {fn arg arg'} (hv : Value fn) (h : Step arg arg') :
Step (.app fn arg) (.app fn arg')
| beta {body arg} (hv : Value arg) : Step (.app (.lam body) arg) (subst 0 arg body)Preservation is where the work lives, and the work is a lemma stack. The key statement, substitution preserves typing, cannot be proved for the outermost binder alone: its induction passes under binders, so it generalizes over a context prefix, and it needs weakening, stated as splicing a block of types into the middle of a context. Two arithmetic facts about shift keep the indices honest along the way:
theorem shift_zero (c : Nat) (e : Exp) : shift c 0 e = e := by
induction e generalizing c with
| var i => simp [shift]
| unit => rfl
| lam body ih => simp [shift, ih]
| app fn arg ihf iha => simp [shift, ihf, iha]
theorem shift_shift (c a b : Nat) (e : Exp) :
shift c a (shift c b e) = shift c (a + b) e := by
induction e generalizing c with
| var i =>
simp only [shift]
by_cases h : i < c
· simp [shift, h]
· simp only [h, if_false]
have : ¬ i + b < c := by omega
simp only [shift, this, if_false]
congr 1
omega
| unit => rfl
| lam body ih => simp [shift, ih]
| app fn arg ihf iha => simp [shift, ihf, iha]/-- Weakening as insertion: a term well typed in `pre ++ post` stays well typed
when a block `mid` is spliced in at depth `pre.length`, provided its variables
are shifted past the inserted block. -/
theorem hasType_shift {pre mid post : List Ty} {t : Exp} {ty : Ty}
(h : HasType (pre ++ post) t ty) :
HasType (pre ++ mid ++ post) (shift pre.length mid.length t) ty := by
induction t generalizing pre ty with
| var i =>
cases h with
| var hv =>
simp only [shift]
by_cases hlt : i < pre.length
· simp only [hlt, if_true]
refine .var ?_
have hlen : i < (pre ++ mid).length := by rw [List.length_append]; omega
rw [List.getElem?_append_left hlt] at hv
rw [List.getElem?_append_left hlen, List.getElem?_append_left hlt]
exact hv
· simp only [hlt, if_false]
refine .var ?_
have hge : pre.length ≤ i := by omega
have hge' : (pre ++ mid).length ≤ i + mid.length := by
rw [List.length_append]; omega
rw [List.getElem?_append_right hge] at hv
rw [List.getElem?_append_right hge',
show (i + mid.length) - (pre ++ mid).length = i - pre.length by
rw [List.length_append]; omega]
exact hv
| unit => cases h; exact .unit
| lam body ih =>
cases h with
| lam hb =>
refine .lam ?_
have := ih (pre := _ :: pre) hb
simpa [shift] using this
| app fn arg ihf iha =>
cases h with
| app hf ha => exact .app (ihf hf) (iha ha)
/-- Substitution preserves typing. `s` is well typed in `post`; substituting it
for the variable that a block starting at `pre.length` would name turns a term
typed in `pre ++ dom :: post` into one typed in `pre ++ post`. -/
theorem hasType_subst {pre post : List Ty} {dom : Ty} {s t : Exp} {ty : Ty}
(ht : HasType (pre ++ dom :: post) t ty) (hs : HasType post s dom) :
HasType (pre ++ post) (subst pre.length (shift 0 pre.length s) t) ty := by
induction t generalizing pre ty with
| var i =>
cases ht with
| var hv =>
simp only [subst]
by_cases hlt : i < pre.length
· simp only [hlt, if_true]
refine .var ?_
rw [List.getElem?_append_left hlt] at hv ⊢
exact hv
· simp only [hlt, if_false]
by_cases heq : i = pre.length
· subst heq
simp only [if_true]
rw [List.getElem?_append_right (Nat.le_refl _)] at hv
simp only [Nat.sub_self, List.getElem?_cons_zero, Option.some.injEq] at hv
subst hv
have := hasType_shift (pre := ([] : List Ty)) (mid := pre) (post := post) hs
simpa using this
· simp only [heq, if_false]
refine .var ?_
have hge : pre.length ≤ i := by omega
have hgt : pre.length < i := by omega
rw [List.getElem?_append_right hge] at hv
rw [List.getElem?_append_right (by omega : pre.length ≤ i - 1)]
have hpos : i - pre.length = (i - 1 - pre.length) + 1 := by omega
rw [hpos, List.getElem?_cons_succ] at hv
exact hv
| unit => cases ht; exact .unit
| lam body ih =>
cases ht with
| lam hb =>
have hih := ih (pre := _ :: pre) hb
simp only [subst]
refine .lam ?_
rw [shift_shift, Nat.add_comm 1 pre.length]
exact hih
| app fn arg ihf iha =>
cases ht with
| app hf ha => exact .app (ihf hf) (iha ha)
theorem preservation {ctx e e' ty}
(ht : HasType ctx e ty) (hs : Step e e') : HasType ctx e' ty := by
induction hs generalizing ty with
| appL _ ih =>
cases ht with
| app hf ha => exact .app (ih hf) ha
| appR _ _ ih =>
cases ht with
| app hf ha => exact .app hf (ih ha)
| beta _ =>
cases ht with
| app hf ha =>
cases hf with
| lam hb =>
have := hasType_subst (pre := ([] : List Ty)) hb ha
simpa [shift_zero] using thisProgress is the shorter half. One observation about canonical forms, a closed value at an arrow type can only be a lambda, and the induction on typing writes itself, every case a value or a step:
/-- A value at an arrow type is a lambda: the canonical-forms half of progress. -/
theorem canonical_arrow {e dom cod} (hv : Value e) (ht : HasType [] e (.arrow dom cod)) :
∃ body, e = .lam body := by
cases hv with
| unit => cases ht
| lam => exact ⟨_, rfl⟩
theorem progress {e ty} (ht : HasType [] e ty) : Value e ∨ ∃ e', Step e e' := by
generalize hctx : ([] : List Ty) = ctx at ht
induction ht with
| var hv => subst hctx; simp at hv
| unit => exact .inl .unit
| lam _ => exact .inl .lam
| app hf ha ihf iha =>
subst hctx
rcases ihf rfl with hvf | ⟨fn', hstep⟩
· rcases iha rfl with hva | ⟨arg', hstep⟩
· obtain ⟨body, rfl⟩ := canonical_arrow hvf hf
exact .inr ⟨_, .beta hva⟩
· exact .inr ⟨_, .appR hvf hstep⟩
· exact .inr ⟨_, .appL hstep⟩The two theorems compose into a checked demonstration on the identity redex: it is well typed and not a value, so progress produces the beta step, and preservation carries the type across it:
/-- `(\x. x) unit`, the identity at `Unit` applied to `unit`. -/
def idRedex : Exp := .app (.lam (.var 0)) .unit
example : HasType [] idRedex .unit := .app (.lam (.var rfl)) .unit
/-- One beta step lands on `unit`, since `subst 0 unit (var 0)` computes to it. -/
example : Step idRedex .unit := .beta .unit
/-- Progress and preservation compose: the well-typed redex is not a value, so
progress hands back a step, and preservation keeps the type across it. -/
example : ∃ e', Step idRedex e' ∧ HasType [] e' .unit := by
have ht : HasType [] idRedex .unit := .app (.lam (.var rfl)) .unit
rcases progress ht with hv | ⟨e', hstep⟩
· cases hv
· exact ⟨e', hstep, preservation ht hstep⟩Metatheory, by construction
There is a second route, and it changes what a theorem is. Make the typing relation the index of the syntax, and the theorems above stop needing statements:
inductive Ty where
| unit
| arrow (dom cod : Ty)
deriving Repr, BEqinductive Var : List Ty -> Ty -> Type where
| here : Var (ty :: ctx) ty
| there (v : Var ctx ty) : Var (ty' :: ctx) tyinductive Term : List Ty -> Ty -> Type where
| var (v : Var ctx ty) : Term ctx ty
| unit : Term ctx .unit
| lam (body : Term (dom :: ctx) cod) : Term ctx (.arrow dom cod)
| app (fn : Term ctx (.arrow dom cod)) (arg : Term ctx dom) : Term ctx codA variable is a proof of membership in the context; an application demands a function whose domain is the argument's type, or it does not typecheck as a Lean term. Evaluation lands directly in Lean's own types, and the function is total: no partial, no fuel, no default cases, because ill-typed and ill-scoped inputs are not filtered out but unrepresentable.
def Ty.denote : Ty -> Type
| .unit => Unit
| .arrow dom cod => dom.denote -> cod.denote
def denoteCtx : List Ty -> Type
| [] => Unit
| ty :: ctx => ty.denote × denoteCtx ctx
def Var.denote : Var ctx ty -> denoteCtx ctx -> ty.denote
| .here, (v, _) => v
| .there x, (_, env) => x.denote env
def Term.denote : Term ctx ty -> denoteCtx ctx -> ty.denote
| .var v, env => v.denote env
| .unit, _ => ()
| .lam body, env => fun arg => body.denote (arg, env)
| .app fn arg, env => (fn.denote env) (arg.denote env)def idUnit : Term [] (.arrow .unit .unit) :=
.lam (.var .here)
def applyId : Term [] .unit :=
.app idUnit .unit
example : applyId.denote () = () := rfl
def constFn : Term [] (.arrow .unit (.arrow .unit .unit)) :=
.lam (.lam (.var (.there .here)))
example : constFn.denote () () () = () := rflCompare the honest disclaimers of chapter 1 and chapter 2: the combinators were partial because inputs could loop, the evaluator was partial because U : U admits terms with no normal form. Here the kernel accepts denote as structurally recursive, and type safety is not a theorem about the interpreter but the type of the interpreter. Even scope errors move from runtime to unwritability:
/--
error: Application type mismatch: The argument
Var.here
has type
Var (?m.4 :: ?m.5) ?m.4
but is expected to have type
Var [] Ty.unit
in the application
Term.var Var.here
-/
#guard_msgs in
def escaped : Term [] .unit := .var .hereThe honest scope note: this is the simply typed fragment, arrow and unit. Intrinsically typed dependent syntax must define the type of terms and the evaluation of types simultaneously, which needs induction-recursion, and Lean does not offer it; that is why chapter 2's checker for the full language is extrinsic, and why the dependent case is qualitatively harder. Together, chapter 5 and this chapter mirror the whole course: the same metalanguage that hosted the object language's syntax turns out strong enough to carry its semantics, proofs included.
The two theorems, as types
A closing exhibit condenses this chapter's title into two Infoview lines. Asked for the types of progress and preservation, Lean answers with the statements themselves, because in a dependently typed language the theorem is the type and the proof scripts above were programs inhabiting them; this is the promise chapter 0 made beside LawfulMonad, kept on the object language:
/-- info: @progress : ∀ {e : Exp} {ty : Ty}, HasType [] e ty → Value e ∨ ∃ e', Step e e' -/
#guard_msgs in
#check @progress
/--
info: @preservation : ∀ {ctx : List Ty} {e e' : Exp} {ty : Ty}, HasType ctx e ty → Step e e' → HasType ctx e' ty
-/
#guard_msgs in
#check @preservationFurther reading
- Programming Language Foundations in Agda, Properties: progress and preservation in Agda, the model both for the extrinsic section above and for the checked-code discipline of these lectures.
- Chapman, Kireev, Nester, and Wadler, System F in Agda, for Fun and Profit: the metatheory game of this chapter played at full size, System F with kinds and recursive types, intrinsically typed throughout.