6. Progress and Preservation

The best way to understand type theory is to implement it!
Anders Mörtberg, Yet Another Cartesian Cubical Type Theory, 2018

The chapter 0 has been advertising since its first sighting of propositions as types: 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, rechecked by Lean in chapter 4, and embedded in Lean since chapter 5; what is missing is a guarantee that its typing discipline means something. This chapter proves type safety twice: extrinsically, the typing a relation about raw terms, then intrinsically, the typing the index of the syntax itself; both times the theorems end up running as an evaluator.

Progress: a closed well-typed term is finished or can move. Given $\vdash t : A$ , either $t$ is a value or $t \longrightarrow t'$ for some $t'$ .
Preservation: a step does not change the type, in any context. Given $\Gamma \vdash t : A$ and $t \longrightarrow t'$ , also $\Gamma \vdash t' : A$ .

Metatheory, extrinsic

Classically the pair is stated about an untyped syntax; this section proves it 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 family, one constructor per rule, with the variable rule reading the context by plain list lookup. One choice deserves its own sentence: the judgment lands in Type, not Prop, so a derivation is data a program can inspect; the consequence arrives with the evaluator below:

inductive Exp where
  | var (i : Nat)
  | unit
  | lam (body : Exp)
  | app (fn arg : Exp)
deriving Repr, BEq

inductive HasType : List Ty -> Exp -> Ty -> Type 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) cod

The variable rule compresses its whole premise into one equation. The lookup ctx[i]? is the standard library's optional indexing: it returns the entry wrapped in some when the index is in bounds and none past the end, so the single hypothesis ctx[i]? = some ty says both that the variable is in scope and that the type it finds is ty. A membership judgment with its own constructors, one for the head of the context and one for skipping an entry, would state the same thing, and the intrinsic section takes exactly that shape for its variables; the equation is chosen here because the lemma stack below splices and appends contexts, and every fact it needs about lookup under ++ is already a library lemma, discharged by rewriting and arithmetic instead of by fresh inductions. The empty context repays the choice once more: there the hypothesis reads none = some ty, which nothing proves, and the variable case of progress below is dismissed by exactly that impossibility.

Substitution, the operation chapter 2 avoided, must now be written down. Normalization by evaluation never substitutes, closures and environments carry that work; small-step reduction (Programming language semantics: it's easy as 1,2,3) 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 -> Type where
  | unit : Value .unit
  | lam {body} : Value (.lam body)

inductive Step : Exp -> Exp -> Type 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. Stationed in Type, each lemma is simultaneously the statement and the code that performs it. 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. -/
def hasTypeShift {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 :=
  match t, h with
  | .var i, .var hv => by
    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, .unit => .unit
  | .lam _, .lam hb => .lam (hasTypeShift (pre := _ :: pre) hb)
  | .app _ _, .app hf ha => .app (hasTypeShift hf) (hasTypeShift 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`. -/
def hasTypeSubst {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 :=
  match t, ht with
  | .var i, .var hv => by
    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 := hasTypeShift (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, .unit => .unit
  | .lam _, .lam hb => by
    have hih := hasTypeSubst (pre := _ :: pre) hb hs
    simp only [subst]
    refine .lam ?_
    rw [shift_shift, Nat.add_comm 1 pre.length]
    exact hih
  | .app _ _, .app hf ha => .app (hasTypeSubst hf hs) (hasTypeSubst ha hs)

def preservation {ctx e e' ty}
    (ht : HasType ctx e ty) (hs : Step e e') : HasType ctx e' ty :=
  match hs, ht with
  | .appL h, .app hf ha => .app (preservation hf h) ha
  | .appR _ h, .app hf ha => .app hf (preservation ha h)
  | .beta _, .app (.lam hb) ha => by
    have := hasTypeSubst (pre := ([] : List Ty)) hb ha
    simpa [shift_zero] using this

Progress is the shorter half, and it ships its own statement: a verdict, done or step, that a later section will run. The induction on the derivation writes itself, each case a value, a step, or an impossibility; canonical forms is the closing match, where a value in function position must be a lambda because the derivation refutes unit:

/-- What progress claims, as data: a verdict a program may inspect. -/
inductive Progress (e : Exp) : Type where
  | done (hv : Value e)
  | step (e' : Exp) (h : Step e e')

/-- Progress, by induction on the derivation: each case a value, a step, or
an impossibility the derivation itself refutes. -/
def progress : HasType [] e ty -> Progress e
  | .var hv => nomatch hv
  | .unit => .done .unit
  | .lam _ => .done .lam
  | .app hf ha =>
    match progress hf with
    | .step _ h => .step _ (.appL h)
    | .done hvf =>
      match progress ha with
      | .step _ h => .step _ (.appR hvf h)
      | .done hva =>
        match hvf with
        | .lam => .step _ (.beta hva)
        | .unit => nomatch hf

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

def idRedexTyped : 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

#guard match progress idRedexTyped with
  | .step e' _ => e' == .unit
  | .done _ => false

/-- Preservation carries the type across the step progress found. -/
example : HasType [] .unit .unit := preservation idRedexTyped (.beta .unit)

The theorems, as an evaluator

The Properties chapter of PLFA ends the story one step further: by repeated application of progress and preservation, a closed well-typed term can be evaluated. Nothing stands between our two proofs and that program, because the judgments were stationed in Type from the start: a Progress verdict is data, and a program may ask which arm it holds. Lean's other sort is the road not taken, and it deserves its price tag: theorems default to Prop, proof-irrelevant and erased before anything runs, where certificates ride for free precisely because nothing can inspect them. Judgments in Prop would have priced this section at a hand-built Type twin of progress, inversion lemmas to feed it, and an existential threaded through the loop; data costs a carried witness instead, and the loop below carries it.

Iteration is where preservation enters the evaluator: each recursive call re-types the stepped term with it. The pair proves nothing about termination, so the loop is bounded by fuel, called gas after PLFA's borrowing from Ethereum, and the verdict reports which ran out first, term or gas, carrying the reduction sequence as a certificate either way. One thing PLFA's verdict carries that ours does not is the arithmetic tying trace length to gas spent; these lectures leave the counting to the pins below:

/-- Zero or more steps: the reflexive-transitive closure of `Step`. -/
inductive Steps : Exp -> Exp -> Type where
  | refl {e} : Steps e e
  | head {e e' e''} (h : Step e e') (hs : Steps e' e'') : Steps e e''

/-- A gas-bounded run ends one of two ways, and either way the reduction
sequence rides along as a certificate. -/
inductive Eval (e : Exp) : Type where
  | outOfGas (e' : Exp) (hs : Steps e e')
  | value (v : Exp) (hs : Steps e v) (hv : Value v)

/-- Iterate progress; preservation re-types the term for every recursive
call. The two proofs establish no termination, so `gas` bounds the loop. -/
def eval (gas : Nat) (ht : HasType [] e ty) : Eval e :=
  match gas with
  | 0 => .outOfGas e .refl
  | gas + 1 =>
    match progress ht with
    | .done hv => .value e .refl hv
    | .step _ hstep =>
      match eval gas (preservation ht hstep) with
      | .outOfGas e'' hs => .outOfGas e'' (.head hstep hs)
      | .value v hs hv => .value v (.head hstep hs) hv

A first pair of pinned runs closes the loop on a gentle term, the identity applied two redexes deep. The verdict as a whole can be neither printed nor compared, its certificates being derivations, so each pin matches one arm and tests the carried term with the derived ==: given gas enough, the evaluator reaches unit; starved at one unit of gas, it spends the inner redex and stops at exactly idRedex:

/-- `(\x. x) ((\x. x) unit)`: the identity applied to `idRedex`, two redexes
deep. -/
def idChain : Exp := .app (.lam (.var 0)) idRedex

def idChainTyped : HasType [] idChain .unit :=
  .app (.lam (.var rfl)) idRedexTyped

#guard match eval 8 idChainTyped with
  | .value v _ _ => v == .unit
  | .outOfGas _ _ => false

#guard match eval 1 idChainTyped with
  | .outOfGas e' _ => e' == idRedex
  | .value _ _ _ => false

Pretty printing, registered

The pins so far compared terms without ever displaying one; the next run should print its term, and the registry of chapter 3 has been waiting for the request: of its six kinds, these lectures have so far registered four, every one but the return leg's pair. The leg first wants the value lifted back into an Expr, the job of a ToExpr instance and the road a plain #eval prefers:

open Lean in
/-- Lift a run-time `Exp` back into the `Expr` denoting it, constructor by
constructor; `#eval` prefers this road whenever it exists. Core could derive
this instance; it is spelled out once to show the encoding. -/
instance : ToExpr Exp where
  toTypeExpr := mkConst ``Exp
  toExpr := go where
    go : Exp -> Expr
      | .var i => mkApp (mkConst ``Exp.var) (toExpr i)
      | .unit => mkConst ``Exp.unit
      | .lam b => mkApp (mkConst ``Exp.lam) (go b)
      | .app f a => mkApp2 (mkConst ``Exp.app) (go f) (go a)

The missing two follow: three unexpanders resugar the constructors, the lambda into a scoped display syntax and the rest into bare indices and juxtaposition, and one delaborator dresses the bare constant; from here on every #eval of an Exp prints in the object language's own spelling, the parenthesizer inserting exactly the brackets the tree never stored:

scoped syntax:10 "\\." term:10 : term

open Lean PrettyPrinter in
/-- A lambda resugars into the display syntax above. -/
@[app_unexpander Exp.lam]
def unexpandLam : Unexpander
  | `($_ $body) => `(\.$body)
  | _ => throw ()

open Lean PrettyPrinter in
/-- A variable resugars into its bare index; only literal indices match,
which is all a reduced closed value can carry. -/
@[app_unexpander Exp.var]
def unexpandVar : Unexpander
  | `($_ $i:num) => `($i:num)
  | _ => throw ()

open Lean PrettyPrinter in
/-- An application resugars into juxtaposition; the parenthesizer supplies
the brackets. -/
@[app_unexpander Exp.app]
def unexpandApp : Unexpander
  | `($_ $fn $arg) => `($fn $arg)
  | _ => throw ()

open Lean PrettyPrinter Delaborator in
/-- The bare constant takes a delaborator, not an unexpander; the emitted
ident deliberately never enters the token table. -/
@[delab app.Course.Chapter6_ProgressAndPreservation.Exp.unit]
def delabExpUnit : Delab := pure (mkIdent `unit)

The workload worth printing is the doubling combinator applied to itself. When chapter 5 instantiated a Church numeral at the type of numerals, it leaned on U : U where a stratified theory would have spent a universe level; the simply typed shadow of that move survives here because the relation types occurrences of the untyped syntax, and twiceTyped is a family of derivations:

/-- The doubling combinator `\f. \x. f (f x)`. -/
def twice : Exp := .lam (.lam (.app (.var 1) (.app (.var 1) (.var 0))))

/-- One untyped term, a family of typings: `twice` checks at every instance
`(a -> a) -> (a -> a)`. -/
def twiceTyped (a : Ty) : HasType [] twice (.arrow (.arrow a a) (.arrow a a)) :=
  .lam (.lam (.app (.var rfl) (.app (.var rfl) (.var rfl))))

The family deserves one look in its native dress. A term of HasType is a natural-deduction derivation written on one line, root first, and unfolding twiceTyped recovers the tree it abbreviates: every bar is one constructor and wears its name, and every leaf is the variable rule, whose lookup equation is exactly the hypothesis each rfl above discharges. Writing $\Gamma$ for $[a,\, a{\to}a]$ , the context the two lambda rules assemble, innermost binder first:

\dfrac{ \dfrac{ \dfrac{ \dfrac{\Gamma[1]? = \mathtt{some}\,(a{\to}a)}{\Gamma \vdash 1 : a{\to}a}\,{\scriptstyle\mathtt{.var}} \quad \dfrac{ \dfrac{\Gamma[1]? = \mathtt{some}\,(a{\to}a)}{\Gamma \vdash 1 : a{\to}a}\,{\scriptstyle\mathtt{.var}} \quad \dfrac{\Gamma[0]? = \mathtt{some}\,a}{\Gamma \vdash 0 : a}\,{\scriptstyle\mathtt{.var}} }{\Gamma \vdash 1\;0 : a}\,{\scriptstyle\mathtt{.app}} }{\Gamma \vdash 1\;(1\;0) : a}\,{\scriptstyle\mathtt{.app}} }{[a{\to}a] \vdash \lambda.\; 1\;(1\;0) \;:\; a \to a}\,{\scriptstyle\mathtt{.lam}} }{[\,] \vdash \lambda.\;\lambda.\; 1\;(1\;0) \;:\; (a \to a) \to (a \to a)}\,{\scriptstyle\mathtt{.lam}}

The self-application gives the two copies of twice different instances, the outer one arrow bigger. The run reaches unit after exactly eleven steps, and the gas pins that count: eleven units die on the doorstep of the value, twelve certify it:

/-- `twice twice (\y. y) unit`: the doubler applied to itself, then run. -/
def twiceTwice : Exp := .app (.app (.app twice twice) (.lam (.var 0))) .unit

/-- Typing the self-application: each occurrence gets its own instance. -/
def twiceTwiceTyped : HasType [] twiceTwice .unit :=
  .app
    (.app
      (.app (twiceTyped (.arrow .unit .unit)) (twiceTyped .unit))
      (.lam (.var rfl)))
    .unit

/-- The term a run reached, however it ended. -/
def Eval.current {e : Exp} : Eval e -> Exp
  | .outOfGas e' _ => e'
  | .value v _ _ => v

#guard match eval 12 twiceTwiceTyped with
  | .value v _ _ => v == .unit
  | .outOfGas _ _ => false

#guard match eval 11 twiceTwiceTyped with
  | .outOfGas e' _ => e' == .unit
  | .value _ _ _ => false

And the four-step stop prints its leftover work through the freshly registered leg:

/-- info: (\.(\.(\.0) ((\.0) 0)) ((\.(\.0) ((\.0) 0)) 0)) unit -/
#guard_msgs in
#eval (eval 4 twiceTwiceTyped).current

Metatheory, intrinsic

A second route to the same safety changes what a theorem is. Make the typing relation the index of the syntax, and the theorems above change character: one will dissolve into a definition's type, the other will keep its statement and lose its lemma stack. The interpreter comes first:

inductive Ty where
  | unit
  | arrow (dom cod : Ty)
deriving Repr, BEq

inductive Var : List Ty -> Ty -> Type where
  | here : Var (ty :: ctx) ty
  | there (v : Var ctx ty) : Var (ty' :: ctx) ty

inductive 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 cod

A 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 () () () = () := rfl

Compare 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 .here

Nothing stops this route from replaying the first section's theorems rather than sidestepping them, and the DeBruijn chapter of PLFA is the model. Renaming and substitution return, no longer lemmas about typing but functions whose types state what the extrinsic route proved; the page of hasTypeSubst becomes the one-line type of Term.subst:

/-- A renaming maps the variables of one context into another. -/
def Ren (ctx ctx' : List Ty) : Type := (ty : Ty) -> Var ctx ty -> Var ctx' ty

/-- Push a renaming under one binder. -/
def Ren.ext (r : Ren ctx ctx') : Ren (a :: ctx) (a :: ctx')
  | _, .here => .here
  | _, .there v => .there (r _ v)

/-- The extrinsic route's renaming lemma, as code: the type states that
renaming preserves typing, and the body performs the renaming. -/
def Term.rename (r : Ren ctx ctx') : Term ctx ty -> Term ctx' ty
  | .var v => .var (r _ v)
  | .unit => .unit
  | .lam body => .lam (body.rename r.ext)
  | .app fn arg => .app (fn.rename r) (arg.rename r)

/-- A substitution maps variables to whole terms. -/
def Sub (ctx ctx' : List Ty) : Type := (ty : Ty) -> Var ctx ty -> Term ctx' ty

/-- Push a substitution under one binder: the bound variable stays itself,
everything else is renamed one deeper. -/
def Sub.exts (s : Sub ctx ctx') : Sub (a :: ctx) (a :: ctx')
  | _, .here => .var .here
  | _, .there v => (s _ v).rename fun _ => .there

/-- The substitution lemma, as code: what `hasTypeSubst` proved, this type
states, and the body performs. -/
def Term.subst (s : Sub ctx ctx') : Term ctx ty -> Term ctx' ty
  | .var v => s _ v
  | .unit => .unit
  | .lam body => .lam (body.subst s.exts)
  | .app fn arg => .app (fn.subst s) (arg.subst s)

/-- The substitution that sends the top variable to `u` and every other
variable to itself. -/
def Sub.top (u : Term ctx a) : Sub (a :: ctx) ctx
  | _, .here => u
  | _, .there v => .var v

/-- Single substitution at the top variable, the beta step's engine. -/
def Term.subst1 (body : Term (a :: ctx) ty) (u : Term ctx a) : Term ctx ty :=
  body.subst (Sub.top u)

Values and reduction return with their types on. The step relation forces both endpoints to share a context and a type, so preservation is not proved but declared; no separate theorem is left to state:

inductive Term.Value : Term ctx ty -> Type where
  | unit : Term.Value .unit
  | lam {body : Term (dom :: ctx) cod} : Term.Value (.lam body)

/-- Both endpoints share `ctx` and `ty`: preservation is not a theorem
here, it is this type. -/
inductive Term.Step : Term ctx ty -> Term ctx ty -> Type where
  | appL {fn fn' : Term ctx (.arrow dom cod)} {arg : Term ctx dom}
      (h : Term.Step fn fn') : Term.Step (.app fn arg) (.app fn' arg)
  | appR {fn : Term ctx (.arrow dom cod)} {arg arg' : Term ctx dom}
      (hv : Term.Value fn) (h : Term.Step arg arg') :
      Term.Step (.app fn arg) (.app fn arg')
  | beta {body : Term (dom :: ctx) cod} {arg : Term ctx dom}
      (hv : Term.Value arg) :
      Term.Step (.app (.lam body) arg) (body.subst1 arg)

Progress alone keeps its statement, and even it travels lighter: the canonical-forms observation is the match on the function position, and the variable case dies of scope instead of a lookup in an empty list:

/-- The verdict, over indexed syntax. -/
inductive Term.Progress (t : Term [] ty) : Type where
  | done (hv : t.Value)
  | step (t' : Term [] ty) (h : t.Step t')

/-- Progress keeps its statement and sheds the derivation: recursion is on
the term itself, the variable case dies of scope, and canonical forms is the
index. -/
def Term.progress : (t : Term [] ty) -> Term.Progress t
  | .var v => nomatch v
  | .unit => .done .unit
  | .lam _ => .done .lam
  | .app fn arg =>
    match Term.progress fn with
    | .step fn' h => .step (.app fn' arg) (.appL h)
    | .done hvf =>
      match Term.progress arg with
      | .step arg' h => .step (.app fn arg') (.appR hvf h)
      | .done hva =>
        match fn, hvf with
        | .lam body, _ => .step (body.subst1 arg) (.beta hva)

/-- One typed beta step; `subst1` computes the endpoint. -/
example : Term.Step applyId .unit := .beta (body := .var .here) .unit

A final pair of Infoview lines closes the comparison: preservation has become the type of Term.Step, and progress states over indexed syntax exactly what it stated over raw syntax:

/-- info: @Term.Step : {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty → Type -/
#guard_msgs in
#check @Term.Step

/-- info: @Term.progress : {ty : Ty} → (t : Term [] ty) → t.Progress -/
#guard_msgs in
#check @Term.progress

The gas evaluator replays too, and the DeBruijn chapter again shows the way: the loop sheds its last piece of bookkeeping, threading no derivation and never invoking preservation, the term being well typed by what it is:

/-- Zero or more typed steps: the certificate, endpoints sharing a type. -/
inductive Term.Steps : Term ctx ty -> Term ctx ty -> Type where
  | refl {t} : Term.Steps t t
  | head {t t' t''} (h : Term.Step t t') (hs : Term.Steps t' t'') :
      Term.Steps t t''

/-- A gas-bounded run, as before, minus every trace of typing bookkeeping:
no derivation to thread, no preservation to invoke; the term is well typed
by what it is. -/
inductive Term.Eval (t : Term [] ty) : Type where
  | outOfGas (t' : Term [] ty) (hs : Term.Steps t t')
  | value (v : Term [] ty) (hs : Term.Steps t v) (hv : Term.Value v)

def Term.eval (gas : Nat) (t : Term [] ty) : Term.Eval t :=
  match gas with
  | 0 => .outOfGas t .refl
  | gas + 1 =>
    match Term.progress t with
    | .done hv => .value t .refl hv
    | .step t' hstep =>
      match Term.eval gas t' with
      | .outOfGas t'' hs => .outOfGas t'' (.head hstep hs)
      | .value v hs hv => .value v (.head hstep hs) hv

The doubler completes the parallel. Intrinsically there is no one term with a family of typings; there is a family of terms, and the metalanguage abstracts the instance:

/-- The doubler, intrinsically: the one untyped term with a family of
typings becomes a family of terms, the instance abstracted in the
metalanguage. -/
def twiceT (a : Ty) : Term [] (.arrow (.arrow a a) (.arrow a a)) :=
  .lam (.lam (.app (.var (.there .here)) (.app (.var (.there .here)) (.var .here))))

Drawing twiceT as its tree makes the change of character visible. With typing the index of the syntax there is nothing to write left of the colon: the judgment shrinks to $\Gamma \vdash A$ , the type of terms at $A$ , and the derivation is the term. The shape is the extrinsic tree's unchanged; only the leaves trade their lookup equations for membership proofs, written $\Gamma \ni A$ after the DeBruijn chapter of PLFA, .here at the head of the context and one .there per entry skipped on the way to the binder:

\dfrac{ \dfrac{ \dfrac{ \dfrac{\dfrac{\dfrac{}{[a{\to}a] \ni a{\to}a}\,{\scriptstyle\mathtt{.here}}}{\Gamma \ni a{\to}a}\,{\scriptstyle\mathtt{.there}}}{\Gamma \vdash a{\to}a}\,{\scriptstyle\mathtt{.var}} \quad \dfrac{ \dfrac{\dfrac{\dfrac{}{[a{\to}a] \ni a{\to}a}\,{\scriptstyle\mathtt{.here}}}{\Gamma \ni a{\to}a}\,{\scriptstyle\mathtt{.there}}}{\Gamma \vdash a{\to}a}\,{\scriptstyle\mathtt{.var}} \quad \dfrac{\dfrac{}{\Gamma \ni a}\,{\scriptstyle\mathtt{.here}}}{\Gamma \vdash a}\,{\scriptstyle\mathtt{.var}} }{\Gamma \vdash a}\,{\scriptstyle\mathtt{.app}} }{\Gamma \vdash a}\,{\scriptstyle\mathtt{.app}} }{[a{\to}a] \vdash a \to a}\,{\scriptstyle\mathtt{.lam}} }{[\,] \vdash (a \to a) \to (a \to a)}\,{\scriptstyle\mathtt{.lam}}

The run is the same eleven steps, pinned at the same doorstep and the same four-gas stop; printing stays with the first route, whose Exp owns the return leg:

def twiceTwiceT : Term [] .unit :=
  .app
    (.app (.app (twiceT (.arrow .unit .unit)) (twiceT .unit))
      (.lam (.var .here)))
    .unit

#guard match Term.eval 12 twiceTwiceT with
  | .value .unit _ _ => true
  | _ => false

#guard match Term.eval 11 twiceTwiceT with
  | .outOfGas .unit _ => true
  | _ => false

#guard match Term.eval 4 twiceTwiceT with
  | .outOfGas (.app _ _) _ => true
  | _ => false

The 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 or one of its stronger relatives, and Lean offers none of them; 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 here the proofs are not merely checked but run, the same programs the evaluator iterates. The intrinsic section printed its indexed twins already; these are the title's own two, as stated on raw syntax, and the promise chapter 0 made is kept twice over on the object language:

/-- info: @progress : {e : Exp} → {ty : Ty} → HasType [] e ty → Progress 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 @preservation

Nothing about the exhibit is ceremonial, and two last constructions press the point. The demonstration of the extrinsic section composed the pair once, on the identity redex; stationed in Type, the two theorems compose into a function: progress decides whether the term steps, and when it does, preservation types the target, which is again exactly what the round consumed, a closed well-typed term. Two rounds walk the two-redex chain to its value, the first stopping at idRedex, and a third declines:

/-- One round of the pair: progress decides whether the term steps, and when
it does, preservation types the target, returning exactly what the round
consumed, a closed well-typed term. `eval` is this round, iterated with gas. -/
def stepOnce (ht : HasType [] e ty) : Option ((e' : Exp) × HasType [] e' ty) :=
  match progress ht with
  | .done _ => none
  | .step e' h => some ⟨e', preservation ht h⟩

#guard match stepOnce idChainTyped with
  | some ⟨e', ht1⟩ =>
    e' == idRedex &&
      match stepOnce ht1 with
      | some ⟨.unit, ht2⟩ => (stepOnce ht2).isNone
      | _ => false
  | none => false

The certificates read back too. A reduction sequence is not an assurance to file away but a list of stations to walk, and the return leg prints the doubler's full descent, the twelve stations the gas pins counted, from self-application down to unit:

/-- The reduction sequence a run carries, whichever way it ended. -/
def Eval.steps {e : Exp} : (ev : Eval e) -> Steps e ev.current
  | .outOfGas _ hs => hs
  | .value _ hs _ => hs

/-- A certificate is data, so it reads back: every station of a reduction
sequence, endpoints included. -/
def Steps.trace {e e' : Exp} (hs : Steps e e') : List Exp :=
  match e, hs with
  | e, .refl => [e]
  | e, .head _ rest => e :: rest.trace

/--
info: [(((\.\.1 (1 0)) (\.\.1 (1 0))) (\.0)) unit, ((\.(\.\.1 (1 0)) ((\.\.1 (1 0)) 0)) (\.0)) unit,
  ((\.\.1 (1 0)) ((\.\.1 (1 0)) (\.0))) unit, ((\.\.1 (1 0)) (\.(\.0) ((\.0) 0))) unit,
  (\.(\.(\.0) ((\.0) 0)) ((\.(\.0) ((\.0) 0)) 0)) unit, (\.(\.0) ((\.0) 0)) ((\.(\.0) ((\.0) 0)) unit),
  (\.(\.0) ((\.0) 0)) ((\.0) ((\.0) unit)), (\.(\.0) ((\.0) 0)) ((\.0) unit), (\.(\.0) ((\.0) 0)) unit,
  (\.0) ((\.0) unit), (\.0) unit, unit]
-/
#guard_msgs in
#eval (eval 12 twiceTwiceTyped).steps.trace