Type Systems

4. Types: Type Systems🔗

Note to developers

LATER: For consistency with the STLC definitions in future chapters, it would be better and simpler to represent numbers by a simple nat, rather than as strings of succ applied to 0 (which also introduces subtleties that are really not the main point here). But the present formulation is not a big problem either.

LATER: Harper's lecture from the Milner symposium would make a good support for this lecture.

LATER: There are a bunch of slides from earlier offerings of CIS500 that might be wonderful additions to the TERSE notes. https://www.seas.upenn.edu/~cis500/cis500-f06/lectures/1002.pdf https://www.seas.upenn.edu/~cis500/cis500-f06/lectures/1004.pdf

Our next major topic is type systems — static program analyses that classify expressions according to the "shapes" of their results. We'll begin with a typed version of the simplest imaginable language, to introduce the basic ideas of types and typing rules and the fundamental theorems about type systems: type preservation and progress. In the next chapter we'll move on to the simply typed lambda-calculus, which lives at the core of every modern functional programming language (including Lean!).

4.1. Typed Arithmetic Expressions🔗

To motivate the discussion of type systems, let's begin as usual with a tiny toy language. We want it to have the potential for programs to go wrong because of runtime type errors, so we endow it with two kinds of data — numbers and booleans — where not every operation is defined on both types of data. For example, program terms like 5 + true and if 42 then 0 else 1 use undefined operator/data-type combinations.

The language definition is completely routine.

4.1.1. Syntax🔗

Here is the syntax of program terms, informally:

t::=true
|false
|if t then t else t
|0
|succ t
|pred t
|iszero t

And here it is formally:

namespace TM inductive Tm where | tru | fls | ite (c t e : Tm) | zero | succ (t : Tm) | pred (t : Tm) | isZero (t : Tm)

4.1.1.1. Notation🔗

Writing terms as raw constructors (.ite .fls .zero (.succ .zero)) gets unreadable quickly. We introduce a concrete syntax so that a term can be written inside <{ … }> — for example <{ if false then 0 else succ 0 }> — mirroring the informal grammar above. A bare identifier is spliced as a Lean term (so a variable t is written just t); ~e escapes an arbitrary Lean expression, and ( … ) groups.

You do not need to understand exactly how the declarations below work; every object language in this book is given its syntax the same way, so it is worth seeing the pattern once:

  • declare_syntax_cat adds a new non-terminal to Lean's grammar — here tm, the terms of this chapter's language.

  • Each syntax directive declares one production of that non-terminal, with annotations fixing precedence, and the last one declares the <{ … }> brackets that let a tm appear where Lean expects a term.

  • macro_rules then translates the resulting syntax forms into the corresponding constructors of Tm.

declare_syntax_cat tm -- The keyword atoms (`true`/`false`/`succ`/`pred`/`iszero`) are parsed as bare -- identifiers and dispatched in the macro below, rather than declared as -- reserved symbols. Reserving them would break ordinary Lean uses of -- `true`/`false` and clash with the constructor/case names `succ`, `pred`. syntax:max num : tm syntax:max ident : tm syntax:75 ident ppHardSpace tm:76 : tm syntax:max "(" tm ")" : tm syntax:max "~" term:max : tm syntax:50 "if " tm:51 " then " tm:51 " else " tm:51 : tm syntax:max "<{ " tm " }>" : term open Lean in macro_rules | `(<{ $n:num }>) => if n.getNat == 0 then `(Tm.zero) else Macro.throwErrorAt n "the only numeric literal in this language is 0" | `(<{ $x:ident }>) => match x.getId.toString with | "true" => `(Tm.tru) | "false" => `(Tm.fls) | _ => `($x) -- a bare identifier is a spliced Lean term (usually a variable) | `(<{ $f:ident $e:tm }>) => match f.getId.toString with | "succ" => `(Tm.succ <{ $e }>) | "pred" => `(Tm.pred <{ $e }>) | "iszero" => `(Tm.isZero <{ $e }>) | _ => Macro.throwErrorAt f s!"unknown operator `{f.getId}`" | `(<{ ($e) }>) => `(<{ $e }>) | `(<{ ~$e }>) => pure e | `(<{ if $c then $t else $e }>) => `(Tm.ite <{ $c }> <{ $t }> <{ $e }>)

A delaborator closes the loop: it walks a Tm value and rebuilds the concrete syntax, so that terms appearing in goals, #check, and #eval output print as <{ … }> rather than as a pile of constructors. (Setting pp.notation false turns it off, revealing the raw constructors.) A Ty prints as Bool or Nat.

Notation encoding: printing terms backopen Lean PrettyPrinter Delaborator SubExpr Parenthesizer in /-- Re-inserts parentheses in `tm` output according to the grammar's precedences. -/ @[category_parenthesizer tm] def tm.parenthesizer : CategoryParenthesizer | prec => do maybeParenthesize `tm true wrapParens prec <| parenthesizeCategoryCore `tm prec where wrapParens (stx : Syntax) : Syntax := Unhygienic.run do let pstx ← `(tm| ($(⟨stx⟩))) return pstx.raw.setInfo (SourceInfo.fromRef stx) open Lean PrettyPrinter Delaborator SubExpr in /-- Rebuild `tm` concrete syntax from a `Tm` term. -/ partial def delabTmInner : DelabM (TSyntax `tm) := do let stx ← match_expr ← getExpr with | Tm.tru => `(tm| $(mkIdent `true):ident) | Tm.fls => `(tm| $(mkIdent `false):ident) | Tm.zero => `(tm| 0) | Tm.succ _ => do `(tm| $(mkIdent `succ):ident $(← withAppArg delabTmInner)) | Tm.pred _ => do `(tm| $(mkIdent `pred):ident $(← withAppArg delabTmInner)) | Tm.isZero _ => do `(tm| $(mkIdent `iszero):ident $(← withAppArg delabTmInner)) | Tm.ite _ _ _ => do let c ← withAppFn <| withAppFn <| withAppArg delabTmInner let t ← withAppFn <| withAppArg delabTmInner let e ← withAppArg delabTmInner `(tm| if $c then $t else $e) | _ => do -- A bare variable prints without the `~` escape; anything else keeps it. match ← delab with | `($i:ident) => `(tm| $i:ident) | e => `(tm| ~$e) (⟨·⟩) <$> annotateTermInfo ⟨stx.raw⟩ open Lean PrettyPrinter Delaborator SubExpr in -- The keys are the constants' full names: `Tm` lives in namespace `TM`, and the -- `delab` attribute does not resolve its argument against the current namespace. @[delab app.TM.Tm.tru, delab app.TM.Tm.fls, delab app.TM.Tm.zero, delab app.TM.Tm.succ, delab app.TM.Tm.pred, delab app.TM.Tm.isZero, delab app.TM.Tm.ite] partial def delabTm : Delab := whenPPOption getPPNotation do guard <| match_expr ← getExpr with | Tm.tru => true | Tm.fls => true | Tm.zero => true | Tm.succ _ => true | Tm.pred _ => true | Tm.isZero _ => true | Tm.ite _ _ _ => true | _ => false match ← delabTmInner with | `(tm| ~$e) => pure e | e => `(<{ $e }>)

4.1.1.2. Values🔗

Values are true, false, and numeric values (0, and succ of a numeric value).

inductive Tm.IsBValue : Tm → Prop where | tru : Tm.IsBValue <{ true }> | fls : Tm.IsBValue <{ false }> inductive Tm.IsNValue : Tm → Prop where | zero : Tm.IsNValue <{ 0 }> | succ (t : Tm) (h : Tm.IsNValue t) : Tm.IsNValue <{ succ t }> def Tm.IsValue (t : Tm) : Prop := Tm.IsBValue t ∨ Tm.IsNValue t

4.1.2. Operational Semantics🔗

Here is the single-step relation, informally.

                   -----------------------------                 (ifTrue)
                   if true then t₁ else t₂ ⟶ t₁

                   ------------------------------                (ifFalse)
                   if false then t₁ else t₂ ⟶ t₂

                              t₁ ⟶ t₁'
            -----------------------------------------------      (ifStep)
            if t₁ then t₂ else t₃ ⟶ if t₁' then t₂ else t₃

                              t₁ ⟶ t₁'
                         -------------------                     (succStep)
                         succ t₁ ⟶ succ t₁'

                           -----------                           (predZero)
                           pred 0 ⟶ 0

                            IsNValue v
                        ------------------                       (predSucc)
                        pred (succ v) ⟶ v

                              t₁ ⟶ t₁'
                         -------------------                     (predStep)
                         pred t₁ ⟶ pred t₁'

                          ----------------                       (isZeroZero)
                          iszero 0 ⟶ true

                             IsNValue v
                      ------------------------                   (isZeroSucc)
                      iszero (succ v) ⟶ false

                              t₁ ⟶ t₁'
                       -----------------------                   (isZeroStep)
                       iszero t₁ ⟶ iszero t₁'

The formal rules are below. We are defining them differently than we have previously: We are using the relation's own notation (⟶) inside the constructors. We achieve this by defining Tm.Step within a section, and within that section using set_option hygiene false on ⟶ so that the constructors read in this syntax; after the section closes, we use a scoped notation as we have done before.

section set_option hygiene false in local notation:40 t:41 " ⟶ " t':41 => Tm.Step t t' inductive Tm.Step : Tm → Tm → Prop where | ifTrue (t₁ t₂ : Tm) : <{ if true then t₁ else t₂ }> ⟶ t₁ | ifFalse (t₁ t₂ : Tm) : <{ if false then t₁ else t₂ }> ⟶ t₂ | ifStep (c c' t₂ t₃ : Tm) (h : c ⟶ c') : <{ if c then t₂ else t₃ }> ⟶ <{ if c' then t₂ else t₃ }> | succStep (t₁ t₁' : Tm) (h : t₁ ⟶ t₁') : <{ succ t₁ }> ⟶ <{ succ t₁' }> | predZero : <{ pred 0 }> ⟶ <{ 0 }> | predSucc (v : Tm) (hv : Tm.IsNValue v) : <{ pred (succ v) }> ⟶ v | predStep (t₁ t₁' : Tm) (h : t₁ ⟶ t₁') : <{ pred t₁ }> ⟶ <{ pred t₁' }> | isZeroZero : <{ iszero 0 }> ⟶ <{ true }> | isZeroSucc (v : Tm) (hv : Tm.IsNValue v) : <{ iszero (succ v) }> ⟶ <{ false }> | isZeroStep (t₁ t₁' : Tm) (h : t₁ ⟶ t₁') : <{ iszero t₁ }> ⟶ <{ iszero t₁' }> end scoped notation:40 t:41 " ⟶ " t':41 => Tm.Step t t'

The Tm.IsNValue premises in predSucc and isZeroSucc are needed for determinism (this will be proved in an optional exercise below).

Notice that the Tm.Step relation doesn't care about whether the expression being stepped makes global sense — it just checks that the operation in the next reduction step is being applied to the right kinds of operands. For example, the term succ true cannot take a step, but the almost as obviously nonsensical term

succ (if true then true else true)

can take a step (once, before becoming stuck).

4.1.3. Normal Forms and Values🔗

The first interesting thing to notice about this Tm.Step relation is that the strong progress theorem from the Smallstep chapter fails here. That is, there are terms that are normal forms (they can't take a step) but not values (they are not included in our definition of possible "results of reduction").

Such terms are stuck.

def Tm.IsNormalForm (t : Tm) : Prop := _root_.IsNormalForm Tm.Step t def Tm.IsStuck (t : Tm) : Prop := Tm.IsNormalForm t ∧ ¬ Tm.IsValue t
Exercise★★(some_term_is_stuck)
theorem some_term_is_stuck : ∃ t, Tm.IsStuck t := ⊢ ∃ t, t.IsStuck solution! ⊢ <{ succ false }>.IsStuck; ⊢ <{ succ false }>.IsNormalForm⊢ ¬<{ succ false }>.IsValue ⊢ <{ succ false }>.IsNormalForm hc:∃ t', <{ succ false }> ⟶ t'⊢ False; t':Tmhstp:<{ succ false }> ⟶ t'⊢ False cases hstp with t₁'✝:Tmh:<{ false }> ⟶ t₁'✝⊢ False All goals completed! 🐙 ⊢ ¬<{ succ false }>.IsValue h:<{ succ false }>.IsValue⊢ False cases h with hb:<{ succ false }>.IsBValue⊢ False All goals completed! 🐙 hn:<{ succ false }>.IsNValue⊢ False cases hn with h:<{ false }>.IsNValue⊢ False All goals completed! 🐙

However, although values and normal forms are not the same in this language, the set of values is a subset of the set of normal forms.

This is important because it shows we did not accidentally define things so that some value could still take a step.

theorem nvalue_is_nf (t : Tm) (h : Tm.IsNValue t) : Tm.IsNormalForm t := t:Tmh:t.IsNValue⊢ t.IsNormalForm induction h with t:Tm⊢ <{ 0 }>.IsNormalForm t:Tmhc:∃ t', <{ 0 }> ⟶ t'⊢ False; t:Tmt':Tmhstp:<{ 0 }> ⟶ t'⊢ False; All goals completed! 🐙 t:Tmt₀:Tmhn₀:t₀.IsNValueih:t₀.IsNormalForm⊢ <{ succ t₀ }>.IsNormalForm t:Tmt₀:Tmhn₀:t₀.IsNValueih:t₀.IsNormalFormhc:∃ t', <{ succ t₀ }> ⟶ t'⊢ False; t:Tmt₀:Tmhn₀:t₀.IsNValueih:t₀.IsNormalFormt':Tmhstp:<{ succ t₀ }> ⟶ t'⊢ False cases hstp with t:Tmt₀:Tmhn₀:t₀.IsNValueih:t₀.IsNormalFormt₁':Tmh:t₀ ⟶ t₁'⊢ False All goals completed! 🐙
Exercise★★★(value_is_nf)

(Hint: You will reach a point in this proof where you need to use an induction to reason about a term that is known to be a numeric value. This induction can be performed either over the term itself or over the evidence that it is a numeric value. The proof goes through in either case, but you will find that one way is quite a bit shorter than the other. For the sake of the exercise, try to complete the proof both ways.)

theorem value_is_nf (t : Tm) (h : Tm.IsValue t) : Tm.IsNormalForm t := t:Tmh:t.IsValue⊢ t.IsNormalForm solution! cases h with t:Tmhb:t.IsBValue⊢ t.IsNormalForm t:Tmhb:t.IsBValuehc:∃ t', t ⟶ t'⊢ False; t:Tmhb:t.IsBValuet':Tmhstp:t ⟶ t'⊢ False; t':Tmhstp:<{ true }> ⟶ t'⊢ Falset':Tmhstp:<{ false }> ⟶ t'⊢ False t':Tmhstp:<{ true }> ⟶ t'⊢ Falset':Tmhstp:<{ false }> ⟶ t'⊢ False All goals completed! 🐙 t:Tmhn:t.IsNValue⊢ t.IsNormalForm All goals completed! 🐙

The "other way" mentioned in the hint proves the same fact by induction on the term itself rather than on the evidence that it is a numeric value. It goes through, but is a bit longer than the nvalue_is_nf route above.

theorem value_is_nf' (t : Tm) (h : Tm.IsValue t) : Tm.IsNormalForm t := t:Tmh:t.IsValue⊢ t.IsNormalForm solution! induction t with h:<{ true }>.IsValue⊢ <{ true }>.IsNormalForm h:<{ true }>.IsValuehc:∃ t', <{ true }> ⟶ t'⊢ False; h:<{ true }>.IsValuet':Tmhstp:<{ true }> ⟶ t'⊢ False; All goals completed! 🐙 h:<{ false }>.IsValue⊢ <{ false }>.IsNormalForm h:<{ false }>.IsValuehc:∃ t', <{ false }> ⟶ t'⊢ False; h:<{ false }>.IsValuet':Tmhstp:<{ false }> ⟶ t'⊢ False; All goals completed! 🐙 c:Tmt₀:Tme:Tmc_ih✝:c.IsValue → c.IsNormalFormt_ih✝:t₀.IsValue → t₀.IsNormalForme_ih✝:e.IsValue → e.IsNormalFormh:<{ if c then t₀ else e }>.IsValue⊢ <{ if c then t₀ else e }>.IsNormalForm cases h with c:Tmt₀:Tme:Tmc_ih✝:c.IsValue → c.IsNormalFormt_ih✝:t₀.IsValue → t₀.IsNormalForme_ih✝:e.IsValue → e.IsNormalFormhb:<{ if c then t₀ else e }>.IsBValue⊢ <{ if c then t₀ else e }>.IsNormalForm All goals completed! 🐙 c:Tmt₀:Tme:Tmc_ih✝:c.IsValue → c.IsNormalFormt_ih✝:t₀.IsValue → t₀.IsNormalForme_ih✝:e.IsValue → e.IsNormalFormhn:<{ if c then t₀ else e }>.IsNValue⊢ <{ if c then t₀ else e }>.IsNormalForm All goals completed! 🐙 h:<{ 0 }>.IsValue⊢ <{ 0 }>.IsNormalForm h:<{ 0 }>.IsValuehc:∃ t', <{ 0 }> ⟶ t'⊢ False; h:<{ 0 }>.IsValuet':Tmhstp:<{ 0 }> ⟶ t'⊢ False; All goals completed! 🐙 t₀:Tmih:t₀.IsValue → t₀.IsNormalFormh:<{ succ t₀ }>.IsValue⊢ <{ succ t₀ }>.IsNormalForm -- The `succ` case is the only one that doesn't immediately present a -- contradiction. Considering how a `succ` term can be a value, it is -- syntactically not a boolean value, but the numeric value case -- requires a bit more work. t₀:Tmih:t₀.IsValue → t₀.IsNormalFormh:<{ succ t₀ }>.IsValuehc:∃ t', <{ succ t₀ }> ⟶ t'⊢ False; t₀:Tmih:t₀.IsValue → t₀.IsNormalFormh:<{ succ t₀ }>.IsValuet':Tmhstp:<{ succ t₀ }> ⟶ t'⊢ False cases hstp with t₀:Tmih:t₀.IsValue → t₀.IsNormalFormh:<{ succ t₀ }>.IsValuet₁':Tmhstp':t₀ ⟶ t₁'⊢ False cases h with t₀:Tmih:t₀.IsValue → t₀.IsNormalFormt₁':Tmhstp':t₀ ⟶ t₁'hb:<{ succ t₀ }>.IsBValue⊢ False All goals completed! 🐙 -- By the IH, if `t₀` is a numeric value, then it can not step. t₀:Tmih:t₀.IsValue → t₀.IsNormalFormt₁':Tmhstp':t₀ ⟶ t₁'hn:<{ succ t₀ }>.IsNValue⊢ False cases hn with t₀:Tmih:t₀.IsValue → t₀.IsNormalFormt₁':Tmhstp':t₀ ⟶ t₁'hn₀:t₀.IsNValue⊢ False All goals completed! 🐙 t₀:Tmt_ih✝:t₀.IsValue → t₀.IsNormalFormh:<{ pred t₀ }>.IsValue⊢ <{ pred t₀ }>.IsNormalForm cases h with t₀:Tmt_ih✝:t₀.IsValue → t₀.IsNormalFormhb:<{ pred t₀ }>.IsBValue⊢ <{ pred t₀ }>.IsNormalForm All goals completed! 🐙 t₀:Tmt_ih✝:t₀.IsValue → t₀.IsNormalFormhn:<{ pred t₀ }>.IsNValue⊢ <{ pred t₀ }>.IsNormalForm All goals completed! 🐙 t₀:Tmt_ih✝:t₀.IsValue → t₀.IsNormalFormh:<{ iszero t₀ }>.IsValue⊢ <{ iszero t₀ }>.IsNormalForm cases h with t₀:Tmt_ih✝:t₀.IsValue → t₀.IsNormalFormhb:<{ iszero t₀ }>.IsBValue⊢ <{ iszero t₀ }>.IsNormalForm All goals completed! 🐙 t₀:Tmt_ih✝:t₀.IsValue → t₀.IsNormalFormhn:<{ iszero t₀ }>.IsNValue⊢ <{ iszero t₀ }>.IsNormalForm All goals completed! 🐙
Exercise★★★(step_deterministic) (Optional)

Use value_is_nf (here, nvalue_is_nf) to show that the Tm.Step relation is also deterministic.

theorem step_deterministic : Deterministic Tm.Step := ⊢ Deterministic Tm.Step solution! x:Tmy₁:Tmy₂:Tmh₁:x ⟶ y₁⊢ x ⟶ y₂ → y₁ = y₂ induction h₁ generalizing y₂ with x:Tmy₁:Tmt₁:Tmt₂:Tmy₂:Tm⊢ <{ if true then t₁ else t₂ }> ⟶ y₂ → t₁ = y₂ x:Tmy₁:Tmt₁:Tmt₂:Tmy₂:Tmh₂:<{ if true then t₁ else t₂ }> ⟶ y₂⊢ t₁ = y₂; cases h₂ with x:Tmy₁:Tmt₁:Tmt₂:Tm⊢ t₁ = t₁ All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₂:Tmc'✝:Tmhc:<{ true }> ⟶ c'✝⊢ t₁ = <{ if c'✝ then t₁ else t₂ }> All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₂:Tmy₂:Tm⊢ <{ if false then t₁ else t₂ }> ⟶ y₂ → t₂ = y₂ x:Tmy₁:Tmt₁:Tmt₂:Tmy₂:Tmh₂:<{ if false then t₁ else t₂ }> ⟶ y₂⊢ t₂ = y₂; cases h₂ with x:Tmy₁:Tmt₁:Tmt₂:Tm⊢ t₂ = t₂ All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₂:Tmc'✝:Tmhc:<{ false }> ⟶ c'✝⊢ t₂ = <{ if c'✝ then t₁ else t₂ }> All goals completed! 🐙 x:Tmy₁:Tmc:Tmc':Tmt₂:Tmt₃:Tmhc:c ⟶ c'ih:∀ (y₂ : Tm), c ⟶ y₂ → c' = y₂y₂:Tm⊢ <{ if c then t₂ else t₃ }> ⟶ y₂ → <{ if c' then t₂ else t₃ }> = y₂ x:Tmy₁:Tmc:Tmc':Tmt₂:Tmt₃:Tmhc:c ⟶ c'ih:∀ (y₂ : Tm), c ⟶ y₂ → c' = y₂y₂:Tmh₂:<{ if c then t₂ else t₃ }> ⟶ y₂⊢ <{ if c' then t₂ else t₃ }> = y₂; cases h₂ with x:Tmy₁:Tmc':Tmt₂:Tmt₃:Tmhc:<{ true }> ⟶ c'ih:∀ (y₂ : Tm), <{ true }> ⟶ y₂ → c' = y₂⊢ <{ if c' then t₂ else t₃ }> = t₂ All goals completed! 🐙 x:Tmy₁:Tmc':Tmt₂:Tmt₃:Tmhc:<{ false }> ⟶ c'ih:∀ (y₂ : Tm), <{ false }> ⟶ y₂ → c' = y₂⊢ <{ if c' then t₂ else t₃ }> = t₃ All goals completed! 🐙 x:Tmy₁:Tmc:Tmc':Tmt₂:Tmt₃:Tmhc:c ⟶ c'ih:∀ (y₂ : Tm), c ⟶ y₂ → c' = y₂c'':Tmhc₂:c ⟶ c''⊢ <{ if c' then t₂ else t₃ }> = <{ if c'' then t₂ else t₃ }> All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂y₂:Tm⊢ <{ succ t₁ }> ⟶ y₂ → <{ succ t₁' }> = y₂ x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂y₂:Tmh₂:<{ succ t₁ }> ⟶ y₂⊢ <{ succ t₁' }> = y₂; cases h₂ with x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂t₁'✝:Tmhs₂:t₁ ⟶ t₁'✝⊢ <{ succ t₁' }> = <{ succ t₁'✝ }> All goals completed! 🐙 x:Tmy₁:Tmy₂:Tm⊢ <{ pred 0 }> ⟶ y₂ → <{ 0 }> = y₂ x:Tmy₁:Tmy₂:Tmh₂:<{ pred 0 }> ⟶ y₂⊢ <{ 0 }> = y₂; cases h₂ with x:Tmy₁:Tm⊢ <{ 0 }> = <{ 0 }> All goals completed! 🐙 x:Tmy₁:Tmt₁'✝:Tmhs:<{ 0 }> ⟶ t₁'✝⊢ <{ 0 }> = <{ pred t₁'✝ }> All goals completed! 🐙 x:Tmy₁:Tmv:Tmhv:v.IsNValuey₂:Tm⊢ <{ pred (succ v) }> ⟶ y₂ → v = y₂ x:Tmy₁:Tmv:Tmhv:v.IsNValuey₂:Tmh₂:<{ pred (succ v) }> ⟶ y₂⊢ v = y₂; cases h₂ with x:Tmy₁:Tmv:Tmhv:v.IsNValuehv✝:v.IsNValue⊢ v = v All goals completed! 🐙 x:Tmy₁:Tmv:Tmhv:v.IsNValuet₁'✝:Tmhs:<{ succ v }> ⟶ t₁'✝⊢ v = <{ pred t₁'✝ }> All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂y₂:Tm⊢ <{ pred t₁ }> ⟶ y₂ → <{ pred t₁' }> = y₂ x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂y₂:Tmh₂:<{ pred t₁ }> ⟶ y₂⊢ <{ pred t₁' }> = y₂; cases h₂ with x:Tmy₁:Tmt₁':Tmhs:<{ 0 }> ⟶ t₁'ih:∀ (y₂ : Tm), <{ 0 }> ⟶ y₂ → t₁' = y₂⊢ <{ pred t₁' }> = <{ 0 }> All goals completed! 🐙 x:Tmy₁:Tmt₁':Tmy₂:Tmhv:y₂.IsNValuehs:<{ succ y₂ }> ⟶ t₁'ih:∀ (y₂_1 : Tm), <{ succ y₂ }> ⟶ y₂_1 → t₁' = y₂_1⊢ <{ pred t₁' }> = y₂ All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂t₁'✝:Tmhs₂:t₁ ⟶ t₁'✝⊢ <{ pred t₁' }> = <{ pred t₁'✝ }> All goals completed! 🐙 x:Tmy₁:Tmy₂:Tm⊢ <{ iszero 0 }> ⟶ y₂ → <{ true }> = y₂ x:Tmy₁:Tmy₂:Tmh₂:<{ iszero 0 }> ⟶ y₂⊢ <{ true }> = y₂; cases h₂ with x:Tmy₁:Tm⊢ <{ true }> = <{ true }> All goals completed! 🐙 x:Tmy₁:Tmt₁'✝:Tmhs:<{ 0 }> ⟶ t₁'✝⊢ <{ true }> = <{ iszero t₁'✝ }> All goals completed! 🐙 x:Tmy₁:Tmv:Tmhv:v.IsNValuey₂:Tm⊢ <{ iszero (succ v) }> ⟶ y₂ → <{ false }> = y₂ x:Tmy₁:Tmv:Tmhv:v.IsNValuey₂:Tmh₂:<{ iszero (succ v) }> ⟶ y₂⊢ <{ false }> = y₂; cases h₂ with x:Tmy₁:Tmv:Tmhv:v.IsNValuehv✝:v.IsNValue⊢ <{ false }> = <{ false }> All goals completed! 🐙 x:Tmy₁:Tmv:Tmhv:v.IsNValuet₁'✝:Tmhs:<{ succ v }> ⟶ t₁'✝⊢ <{ false }> = <{ iszero t₁'✝ }> All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂y₂:Tm⊢ <{ iszero t₁ }> ⟶ y₂ → <{ iszero t₁' }> = y₂ x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂y₂:Tmh₂:<{ iszero t₁ }> ⟶ y₂⊢ <{ iszero t₁' }> = y₂; cases h₂ with x:Tmy₁:Tmt₁':Tmhs:<{ 0 }> ⟶ t₁'ih:∀ (y₂ : Tm), <{ 0 }> ⟶ y₂ → t₁' = y₂⊢ <{ iszero t₁' }> = <{ true }> All goals completed! 🐙 x:Tmy₁:Tmt₁':Tmv✝:Tmhv:v✝.IsNValuehs:<{ succ v✝ }> ⟶ t₁'ih:∀ (y₂ : Tm), <{ succ v✝ }> ⟶ y₂ → t₁' = y₂⊢ <{ iszero t₁' }> = <{ false }> All goals completed! 🐙 x:Tmy₁:Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (y₂ : Tm), t₁ ⟶ y₂ → t₁' = y₂t₁'✝:Tmhs₂:t₁ ⟶ t₁'✝⊢ <{ iszero t₁' }> = <{ iszero t₁'✝ }> All goals completed! 🐙
Quiz

Is the following term stuck?

iszero (if true then (succ 0) else 0)

(A) Yes (B) No

Show solution

(B) No

Quiz

What about this one? Is it stuck?

if (succ 0) then true else false

(A) Yes (B) No

Show solution

(A) Yes

Quiz

What about this one? Is it stuck?

succ (succ 0)

(A) Yes (B) No

Show solution

(B) No

Quiz

What about this one? Is it stuck?

succ (if true then true else true)

(A) Yes (B) No

(Hint: Notice that the Tm.Step relation doesn't care about whether the expression being stepped makes global sense — it just checks that the operation in the next reduction step is being applied to the right kinds of operands.)

Show solution

(B) No

Optional aside, good practice with step relations but tangential to the main development. We define an alternate step relation ⇢ and a step function for it.

Note to developers (mwhicks1)
In the Rocq source these were a hidden, never-uncommented draft
(with `eval` still to be renamed to `step`).  Here they are activated as
live Lean. Not sure if we want to keep this.

Suppose we define an alternate single-step relation, written t ⇢ t', that drops the Tm.IsNValue premise from the predSucc and isZeroSucc rules — so pred (succ t) and iszero (succ t) may step even when t is not a numeric value. (It is built with exactly the same notation setup as Tm.Step; note predSucc/isZeroSucc no longer take a premise.)

section set_option hygiene false in local notation:40 t:41 " ⇢ " t':41 => Tm.AltStep t t' inductive Tm.AltStep : Tm → Tm → Prop where | ifTrue (t₁ t₂ : Tm) : <{ if true then t₁ else t₂ }> ⇢ t₁ | ifFalse (t₁ t₂ : Tm) : <{ if false then t₁ else t₂ }> ⇢ t₂ | ifStep (t₁ t₁' t₂ t₃ : Tm) : t₁ ⇢ t₁' → <{ if t₁ then t₂ else t₃ }> ⇢ <{ if t₁' then t₂ else t₃ }> | succStep (t₁ t₁' : Tm) : t₁ ⇢ t₁' → <{ succ t₁ }> ⇢ <{ succ t₁' }> | predZero : <{ pred 0 }> ⇢ <{ 0 }> | predSucc (t₁ : Tm) : <{ pred (succ t₁) }> ⇢ t₁ | predStep (t₁ t₁' : Tm) : t₁ ⇢ t₁' → <{ pred t₁ }> ⇢ <{ pred t₁' }> | isZeroZero : <{ iszero 0 }> ⇢ <{ true }> | isZeroSucc (t₁ : Tm) : <{ iszero (succ t₁) }> ⇢ <{ false }> | isZeroStep (t₁ t₁' : Tm) : t₁ ⇢ t₁' → <{ iszero t₁ }> ⇢ <{ iszero t₁' }> end scoped notation:40 t:41 " ⇢ " t':41 => Tm.AltStep t t'

Some questions about this relation (answers inline):

  • Is ⇢ deterministic (∀ t t' t'', t ⇢ t' → t ⇢ t'' → t' = t'')? No: pred (succ (pred 0)) steps to both pred 0 (by predSucc) and pred (succ 0) (by predStep, since pred 0 ⇢ 0).

  • Is every Tm.Step normal form also a ⇢ normal form? No: pred (succ true) is stuck for Tm.Step but steps under ⇢ (to true, by predSucc, now that the Tm.IsNValue premise is gone).

  • Is every ⇢ normal form also a Tm.Step normal form? Yes — Tm.Step is a subrelation of ⇢, so anything stuck for ⇢ is stuck for Tm.Step.

  • Is every value reachable by Tm.Step (in many steps) also reachable by ⇢ (in many steps)? Yes, for the same subrelation reason.

  • Conversely? No: iszero (succ true) reaches the value false under ⇢ but is stuck under Tm.Step.

A functional version computes a single ⇢ step of a term, returning none when the term is a ⇢ normal form. This is a nice chance to see a step function, which the chapter otherwise gives only as a relation:

def alt_simplify_step (t : Tm) : Option Tm := match t with | <{ if t₁ then t₂ else t₃ }> => match alt_simplify_step t₁ with | some t₁' => some <{ if t₁' then t₂ else t₃ }> | none => match t₁ with | <{ true }> => some t₂ | <{ false }> => some t₃ | _ => none | <{ succ t₁ }> => match alt_simplify_step t₁ with | some t₁' => some <{ succ t₁' }> | none => none | <{ pred t₁ }> => match alt_simplify_step t₁ with | some t₁' => some <{ pred t₁' }> | none => match t₁ with | <{ 0 }> => some <{ 0 }> | <{ succ t₂ }> => some t₂ | _ => none | <{ iszero t₁ }> => match alt_simplify_step t₁ with | some t₁' => some <{ iszero t₁' }> | none => match t₁ with | <{ 0 }> => some <{ true }> | <{ succ Variable name `t₂` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _t₂ Note: This linter can be disabled with `set_option linter.unusedVariables false`t₂ }> => some <{ false }> | _ => none | _ => none -- `pred (succ true)` steps under `⇢` (the dropped `IsNValue` premise) even -- though it is stuck under `Tm.Step`: example : alt_simplify_step <{ pred (succ true) }> = some <{ true }> := rfl example : alt_simplify_step <{ if true then 0 else succ 0 }> = some <{ 0 }> := rfl example : alt_simplify_step <{ 0 }> = none := rfl

4.1.4. Typing🔗

The next critical observation is that, although this language has stuck terms, they are always nonsensical, mixing booleans and numbers in a way that we don't even want to have a meaning. We can easily exclude such ill-typed terms by defining a typing relation that relates terms to the types (either numeric or boolean) of their final results.

The typing relation ⊢ t ⦂ τ relates terms to the types of their results. In informal notation it is often written ⊢ t ⦂ τ and pronounced "t has type τ." The ⊢ symbol is called a "turnstile." The ⦂ between the term and its type is a dedicated type-colon glyph (distinct from an ordinary :); in the editor you enter it with the Lean input abbreviation \tc followed by a space. Below, we're going to see richer typing relations where one or more additional "context" arguments are written to the left of the turnstile. For the moment, the context is always empty.

                     -------------                (tru)
                     ⊢ true ⦂ Bool

                     --------------               (fls)
                     ⊢ false ⦂ Bool

          ⊢ t₁ ⦂ Bool    ⊢ t₂ ⦂ τ    ⊢ t₃ ⦂ τ
          -----------------------------------     (ite)
              ⊢ if t₁ then t₂ else t₃ ⦂ τ

                       ---------                  (zero)
                       ⊢ 0 ⦂ Nat

                      ⊢ t₁ ⦂ Nat
                    ---------------               (succ)
                    ⊢ succ t₁ ⦂ Nat

                      ⊢ t₁ ⦂ Nat
                    ---------------               (pred)
                    ⊢ pred t₁ ⦂ Nat

                      ⊢ t₁ ⦂ Nat
                   ------------------             (isZero)
                   ⊢ iszero t₁ ⦂ Bool

Here are the formal rules.

The typing judgment is written <{ ⊢ t ⦂ T }>: the whole judgment is wrapped in <{ … }>, the term is in the object grammar (bare variables, no inner <{ }>) and the type as Bool/Nat (a type variable is spliced, ~T escapes to a Lean Ty). As with Tm.Step, we define the relation using its own notation. The detailed definition of the notation is folded into the box below.

inductive Ty where | bool | nat syntax:max "<{ " "⊢ " tm " ⦂ " ident " }>" : term syntax:max "<{ " "⊢ " tm " ⦂ " "~" term:max " }>" : term
Notation encoding: typing relation

The notation is defined inside a section with set_option hygiene false so the bare name Tm.HasType in the expansion resolves to the relation being defined; after the section we re-declare the same rules hygienically for real use. Unlike ⟶, the judgment builds on the custom tm syntactic category, so it must use syntax/macro_rules rather than notation — which is why it still needs the app_unexpander to print the judgment back.

section set_option hygiene false in local macro_rules | `(<{ ⊢ $t ⦂ $T:ident }>) => match T.getId.toString with | "Bool" => `(Tm.HasType <{ $t }> Ty.bool) | "Nat" => `(Tm.HasType <{ $t }> Ty.nat) | _ => `(Tm.HasType <{ $t }> $T) | `(<{ ⊢ $t ⦂ ~$T }>) => `(Tm.HasType <{ $t }> $T)
-- The actual definition, written in the notation above. inductive Tm.HasType : Tm → Ty → Prop where | tru : <{ ⊢ true ⦂ Bool }> | fls : <{ ⊢ false ⦂ Bool }> | ite (t₁ t₂ t₃ : Tm) (τ : Ty) (h₁ : <{ ⊢ t₁ ⦂ Bool }>) (h₂ : <{ ⊢ t₂ ⦂ τ }>) (h₃ : <{ ⊢ t₃ ⦂ τ }>) : <{ ⊢ if t₁ then t₂ else t₃ ⦂ τ }> | zero : <{ ⊢ 0 ⦂ Nat }> | succ (t₁ : Tm) (h : <{ ⊢ t₁ ⦂ Nat }>) : <{ ⊢ succ t₁ ⦂ Nat }> | pred (t₁ : Tm) (h : <{ ⊢ t₁ ⦂ Nat }>) : <{ ⊢ pred t₁ ⦂ Nat }> | isZero (t₁ : Tm) (h : <{ ⊢ t₁ ⦂ Nat }>) : <{ ⊢ iszero t₁ ⦂ Bool }>
Notation encoding: typing relation-- The same rules repeated with hygiene enabled, for use after the section. macro_rules | `(<{ ⊢ $t ⦂ $T:ident }>) => match T.getId.toString with | "Bool" => `(Tm.HasType <{ $t }> Ty.bool) | "Nat" => `(Tm.HasType <{ $t }> Ty.nat) | _ => `(Tm.HasType <{ $t }> $T) | `(<{ ⊢ $t ⦂ ~$T }>) => `(Tm.HasType <{ $t }> $T) -- Print `Tm.HasType`/`Ty` values back as `<{ ⊢ … ⦂ … }>` notation: `delabTy` open Lean PrettyPrinter Delaborator SubExpr in @[delab app.TM.Ty.bool, delab app.TM.Ty.nat] def delabTy : Delab := whenPPOption getPPNotation do match_expr ← getExpr with | Ty.bool => `($(mkIdent `Bool):ident) | Ty.nat => `($(mkIdent `Nat):ident) | _ => failure @[app_unexpander Tm.HasType] def Tm.HasType.unexpand : Lean.PrettyPrinter.Unexpander | `($_ <{ $t }> $T:ident) => `(<{ ⊢ $t ⦂ $T }>) | `($_ $t:ident $T:ident) => `(<{ ⊢ $(⟨t.raw⟩) ⦂ $T }>) | `($_ $t $T) => `(<{ ⊢ ~$t ⦂ ~$T }>) | _ => throw () end
example : <{ ⊢ if false then 0 else succ 0 ⦂ Nat }> := .ite _ _ _ _ .fls .zero (.succ _ .zero)

It's important to realize that the typing relation is a conservative (or static) approximation: it does not consider what happens when the term is reduced — in particular, it does not calculate the type of its normal form.

example : ¬ <{ ⊢ if false then 0 else true ⦂ Bool }> := ⊢ ¬<{ ⊢ if false then 0 else true ⦂ Bool }> hc:<{ ⊢ if false then 0 else true ⦂ Bool }>⊢ False; cases hc with h₁:<{ ⊢ false ⦂ Bool }>h₂:<{ ⊢ 0 ⦂ Bool }>h₃:<{ ⊢ true ⦂ Bool }>⊢ False All goals completed! 🐙 example : ¬ <{ ⊢ if iszero (succ 0) then succ false else true ⦂ Bool }> := ⊢ ¬<{ ⊢ if iszero (succ 0) then succ false else true ⦂ Bool }> hc:<{ ⊢ if iszero (succ 0) then succ false else true ⦂ Bool }>⊢ False; cases hc with h₁:<{ ⊢ iszero (succ 0) ⦂ Bool }>h₂:<{ ⊢ succ false ⦂ Bool }>h₃:<{ ⊢ true ⦂ Bool }>⊢ False All goals completed! 🐙
Exercise★(succ_hastype_nat__hastype_nat) (Optional)
example (t : Tm) (h : <{ ⊢ succ t ⦂ Nat }>) : <{ ⊢ t ⦂ Nat }> := t:Tmh:<{ ⊢ succ t ⦂ Nat }>⊢ <{ ⊢ t ⦂ Nat }> solution! cases h with t:Tmhh:<{ ⊢ t ⦂ Nat }>⊢ <{ ⊢ t ⦂ Nat }> All goals completed! 🐙

4.1.5. Canonical forms🔗

The following two lemmas capture the fundamental fact that the definitions of boolean and numeric values agree with the typing relation: a well-typed value of type Bool is a boolean value, and of type Nat a numeric value.

theorem bool_canonical (t : Tm) (hT : <{ ⊢ t ⦂ Bool }>) (hv : Tm.IsValue t) : Tm.IsBValue t := t:TmhT:<{ ⊢ t ⦂ Bool }>hv:t.IsValue⊢ t.IsBValue cases hv with t:TmhT:<{ ⊢ t ⦂ Bool }>hb:t.IsBValue⊢ t.IsBValue All goals completed! 🐙 t:TmhT:<{ ⊢ t ⦂ Bool }>hn:t.IsNValue⊢ t.IsBValue cases hn with hT:<{ ⊢ 0 ⦂ Bool }>⊢ <{ 0 }>.IsBValue All goals completed! 🐙 t₀:Tmh:t₀.IsNValuehT:<{ ⊢ succ t₀ ⦂ Bool }>⊢ <{ succ t₀ }>.IsBValue All goals completed! 🐙 theorem nat_canonical (t : Tm) (hT : <{ ⊢ t ⦂ Nat }>) (hv : Tm.IsValue t) : Tm.IsNValue t := t:TmhT:<{ ⊢ t ⦂ Nat }>hv:t.IsValue⊢ t.IsNValue cases hv with t:TmhT:<{ ⊢ t ⦂ Nat }>hb:t.IsBValue⊢ t.IsNValue hT:<{ ⊢ true ⦂ Nat }>⊢ <{ true }>.IsNValuehT:<{ ⊢ false ⦂ Nat }>⊢ <{ false }>.IsNValue hT:<{ ⊢ true ⦂ Nat }>⊢ <{ true }>.IsNValuehT:<{ ⊢ false ⦂ Nat }>⊢ <{ false }>.IsNValue All goals completed! 🐙 t:TmhT:<{ ⊢ t ⦂ Nat }>hn:t.IsNValue⊢ t.IsNValue All goals completed! 🐙

4.1.6. Progress🔗

The typing relation enjoys two critical properties.

The first is that well-typed normal forms are not stuck — or conversely, if a term is well typed, then either it is a value or it can take at least one step. We call this progress.

Exercise★★★(finish_progress)

Complete the formal proof of the progress property. (Make sure you understand the parts we've given of the informal proof in the following exercise before starting — this will save you a lot of time.)

theorem progress (t : Tm) (τ : Ty) (hT : <{ ⊢ t ⦂ τ }>) : Tm.IsValue t ∨ ∃ t', t ⟶ t' := t:Tmτ:TyhT:<{ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t' solution! induction hT with t:Tmτ:Ty⊢ <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t' All goals completed! 🐙 t:Tmτ:Ty⊢ <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t' All goals completed! 🐙 t:Tmτ:Ty⊢ <{ 0 }>.IsValue ∨ ∃ t', <{ 0 }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₁:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t'⊢ <{ if t₁ then t₂ else t₃ }>.IsValue ∨ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₁:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t'⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' cases ih₁ with t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hv₁:t₁.IsValue⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' cases bool_canonical t₁ h₁ hv₁ with t:Tmτ:Tyt₂:Tmt₃:TmT:Tyh₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ⊢ true ⦂ Bool }>hv₁:<{ true }>.IsValue⊢ ∃ t', <{ if true then t₂ else t₃ }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₂:Tmt₃:TmT:Tyh₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ⊢ false ⦂ Bool }>hv₁:<{ false }>.IsValue⊢ ∃ t', <{ if false then t₂ else t₃ }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hs₁:∃ t', t₁ ⟶ t'⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:t₃.IsValue ∨ ∃ t', t₃ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'⊢ <{ succ t₁ }>.IsValue ∨ ∃ t', <{ succ t₁ }> ⟶ t' cases ih with t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>hv:t₁.IsValue⊢ <{ succ t₁ }>.IsValue ∨ ∃ t', <{ succ t₁ }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>hs:∃ t', t₁ ⟶ t'⊢ <{ succ t₁ }>.IsValue ∨ ∃ t', <{ succ t₁ }> ⟶ t' t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>t':Tmh':t₁ ⟶ t'⊢ <{ succ t₁ }>.IsValue ∨ ∃ t', <{ succ t₁ }> ⟶ t'; All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'⊢ <{ pred t₁ }>.IsValue ∨ ∃ t', <{ pred t₁ }> ⟶ t' t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'⊢ ∃ t', <{ pred t₁ }> ⟶ t' cases ih with t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>hv:t₁.IsValue⊢ ∃ t', <{ pred t₁ }> ⟶ t' cases nat_canonical t₁ h hv with t:Tmτ:Tyh:<{ ⊢ 0 ⦂ Nat }>hv:<{ 0 }>.IsValue⊢ ∃ t', <{ pred 0 }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₀:Tmhn₀:t₀.IsNValueh:<{ ⊢ succ t₀ ⦂ Nat }>hv:<{ succ t₀ }>.IsValue⊢ ∃ t', <{ pred (succ t₀) }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>hs:∃ t', t₁ ⟶ t'⊢ ∃ t', <{ pred t₁ }> ⟶ t' t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>t':Tmh':t₁ ⟶ t'⊢ ∃ t', <{ pred t₁ }> ⟶ t'; All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'⊢ <{ iszero t₁ }>.IsValue ∨ ∃ t', <{ iszero t₁ }> ⟶ t' t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:t₁.IsValue ∨ ∃ t', t₁ ⟶ t'⊢ ∃ t', <{ iszero t₁ }> ⟶ t' cases ih with t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>hv:t₁.IsValue⊢ ∃ t', <{ iszero t₁ }> ⟶ t' cases nat_canonical t₁ h hv with t:Tmτ:Tyh:<{ ⊢ 0 ⦂ Nat }>hv:<{ 0 }>.IsValue⊢ ∃ t', <{ iszero 0 }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₀:Tmhn₀:t₀.IsNValueh:<{ ⊢ succ t₀ ⦂ Nat }>hv:<{ succ t₀ }>.IsValue⊢ ∃ t', <{ iszero (succ t₀) }> ⟶ t' All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>hs:∃ t', t₁ ⟶ t'⊢ ∃ t', <{ iszero t₁ }> ⟶ t' t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>t':Tmh':t₁ ⟶ t'⊢ ∃ t', <{ iszero t₁ }> ⟶ t'; All goals completed! 🐙
Quiz

What is the relation between the progress property defined here and the strong progress from the Smallstep chapter?

(A) No difference — they mean the same thing

(B) Progress implies strong progress

(C) Strong progress implies progress

(D) No relationship

(E) Dunno

Show solution

(C) Strong progress implies progress

Exercise★★★(finish_progress_informal) (Optional, Manually graded)

Complete the corresponding informal proof.

Note to developers (Benjamin Pierce @bcpierce00)

Check the typesetting of this...

Theorem: If ⊢ t ⦂ T, then either t is a value or else t ⟶ t' for some t'.

Proof: By induction on a derivation of ⊢ t ⦂ T.

  • If the last rule in the derivation is ite, then t = if t₁ then t₂ else t₃, with ⊢ t₁ ⦂ Bool, ⊢ t₂ ⦂ T and ⊢ t₃ ⦂ T. By the IH, either t₁ is a value or else t₁ can step to some t₁'.

    • If t₁ is a value, then by the canonical forms lemmas and the fact that ⊢ t₁ ⦂ Bool we have that t₁ is a boolean value (Tm.IsBValue) — i.e., it is either true or false. If t₁ = true, then t steps to t₂ by ifTrue, while if t₁ = false, then t steps to t₃ by ifFalse. Either way, t can step, which is what we wanted to show.

    • If t₁ itself can take a step, then, by ifStep, so can t.

- If the last rule in the derivation is `tru`, then `t = true`, which
  is a boolean value and hence a value.  The cases for `fls` and `zero`
  are similar.

- If the last rule in the derivation is `succ`, then `t = succ t₁`, with
  `⊢ t₁ ⦂ Nat`.  By the IH, either `t₁` is a value or else `t₁` can step
  to some `t₁'`.

  - If `t₁` is a value, then by the canonical forms lemma `t₁` is an
    `nvalue`, and hence `t` is also an `nvalue` (and hence a value) by
    `succ`.

  - If `t₁` can take a step, then by `succStep`, so can `t`.

- If the last rule in the derivation is `pred`, then `t = pred t₁`, with
  `⊢ t₁ ⦂ Nat`.  By the IH, either `t₁` is a value or else `t₁` can step
  to some `t₁'`.

  - If `t₁` is a value, then (by the same argument as in the previous
    case) it must be an `nvalue`.  By case analysis on the `nvalue`
    judgement, there are two cases:

    - If `t₁ = 0`, then `t` can take a step by `predZero`.

    - Otherwise, `t₁ = succ t₁'`, with `t₁'` an `nvalue`.  Hence `t` can
      again take a step, this time by `predSucc`.

  - Finally, if `t₁` can take a step, then by `predStep`, so can `t`.

- If the last rule in the derivation is `isZero`, then `t = iszero t₁`,
  with `⊢ t₁ ⦂ Nat`.  By the IH, either `t₁` is a value or else `t₁` steps
  to some `t₁'`.

  - If `t₁` is a value, it must be an `nvalue`, and there are two cases to
    consider:

    - If `t₁ = 0`, then `t` can take a step by `isZeroZero`.

    - Otherwise, `t₁ = succ t₁'` where `t₁'` is an `nvalue`.  Hence `t` can
      take a step by `isZeroSucc`.

  - If `t₁` can take a step, then so can `t`, by `isZeroStep`.

This theorem is more interesting than the strong progress theorem that we saw in the Smallstep chapter, where all normal forms were values. Here a term can be stuck, but only if it is ill typed.

Quiz

Quick review: in the language defined at the start of this chapter...

  • Every well-typed normal form is a value.

(A) True (B) False

Show solution

TRUE: This is the content of the progress theorem.

Quiz

In this language...

  • Every value is a normal form.

(A) True (B) False

Show solution

TRUE: This can be proved by induction on values.

Quiz

In this language...

  • The single-step reduction relation is a partial function (i.e., it is deterministic).

(A) True (B) False

Show solution

TRUE: This is the determinism theorem.

Quiz

In this language...

  • The single-step reduction relation is a total function.

(A) True (B) False

Show solution

FALSE: normal forms do not reduce to anything.

4.1.7. Type Preservation🔗

The second critical property of typing is that, when a well-typed term takes a step, the result is a well-typed term (of the same type).

Exercise★★(finish_preservation)

Complete the formal proof of the preservation property. (Again, make sure you understand the informal proof fragment in the following exercise first.)

theorem preservation (t t' : Tm) (τ : Ty) (hT : <{ ⊢ t ⦂ τ }>) (he : t ⟶ t') : <{ ⊢ t' ⦂ τ }> := t:Tmt':Tmτ:TyhT:<{ ⊢ t ⦂ τ }>he:t ⟶ t'⊢ <{ ⊢ t' ⦂ τ }> solution! induction hT generalizing t' with t:Tmτ:Tyt':Tmhe:<{ true }> ⟶ t'⊢ <{ ⊢ t' ⦂ Bool }> All goals completed! 🐙 t:Tmτ:Tyt':Tmhe:<{ false }> ⟶ t'⊢ <{ ⊢ t' ⦂ Bool }> All goals completed! 🐙 t:Tmτ:Tyt':Tmhe:<{ 0 }> ⟶ t'⊢ <{ ⊢ t' ⦂ Nat }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → <{ ⊢ t' ⦂ T }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → <{ ⊢ t' ⦂ T }>t':Tmhe:<{ if t₁ then t₂ else t₃ }> ⟶ t'⊢ <{ ⊢ t' ⦂ T }> cases he with t:Tmτ:Tyt₂:Tmt₃:TmT:Tyh₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → <{ ⊢ t' ⦂ T }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → <{ ⊢ t' ⦂ T }>h₁:<{ ⊢ true ⦂ Bool }>ih₁:∀ (t' : Tm), <{ true }> ⟶ t' → <{ ⊢ t' ⦂ Bool }>⊢ <{ ⊢ t₂ ⦂ T }> All goals completed! 🐙 t:Tmτ:Tyt₂:Tmt₃:TmT:Tyh₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → <{ ⊢ t' ⦂ T }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → <{ ⊢ t' ⦂ T }>h₁:<{ ⊢ false ⦂ Bool }>ih₁:∀ (t' : Tm), <{ false }> ⟶ t' → <{ ⊢ t' ⦂ Bool }>⊢ <{ ⊢ t₃ ⦂ T }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmt₂:Tmt₃:TmT:Tyh₁:<{ ⊢ t₁ ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ T }>h₃:<{ ⊢ t₃ ⦂ T }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → <{ ⊢ t' ⦂ T }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → <{ ⊢ t' ⦂ T }>c':Tmhc:t₁ ⟶ c'⊢ <{ ⊢ if c' then t₂ else t₃ ⦂ T }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Nat }>t':Tmhe:<{ succ t₁ }> ⟶ t'⊢ <{ ⊢ t' ⦂ Nat }> cases he with t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Nat }>t₁':Tmhs:t₁ ⟶ t₁'⊢ <{ ⊢ succ t₁' ⦂ Nat }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Nat }>t':Tmhe:<{ pred t₁ }> ⟶ t'⊢ <{ ⊢ t' ⦂ Nat }> cases he with t:Tmτ:Tyh:<{ ⊢ 0 ⦂ Nat }>ih:∀ (t' : Tm), <{ 0 }> ⟶ t' → <{ ⊢ t' ⦂ Nat }>⊢ <{ ⊢ 0 ⦂ Nat }> All goals completed! 🐙 t:Tmτ:Tyt':Tmhv:t'.IsNValueh:<{ ⊢ succ t' ⦂ Nat }>ih:∀ (t'_1 : Tm), <{ succ t' }> ⟶ t'_1 → <{ ⊢ t'_1 ⦂ Nat }>⊢ <{ ⊢ t' ⦂ Nat }> cases h with t:Tmτ:Tyt':Tmhv:t'.IsNValueih:∀ (t'_1 : Tm), <{ succ t' }> ⟶ t'_1 → <{ ⊢ t'_1 ⦂ Nat }>hh:<{ ⊢ t' ⦂ Nat }>⊢ <{ ⊢ t' ⦂ Nat }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Nat }>t₁':Tmhs:t₁ ⟶ t₁'⊢ <{ ⊢ pred t₁' ⦂ Nat }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Nat }>t':Tmhe:<{ iszero t₁ }> ⟶ t'⊢ <{ ⊢ t' ⦂ Bool }> cases he with t:Tmτ:Tyh:<{ ⊢ 0 ⦂ Nat }>ih:∀ (t' : Tm), <{ 0 }> ⟶ t' → <{ ⊢ t' ⦂ Nat }>⊢ <{ ⊢ true ⦂ Bool }> All goals completed! 🐙 t:Tmτ:Tyv:Tmhv:v.IsNValueh:<{ ⊢ succ v ⦂ Nat }>ih:∀ (t' : Tm), <{ succ v }> ⟶ t' → <{ ⊢ t' ⦂ Nat }>⊢ <{ ⊢ false ⦂ Bool }> All goals completed! 🐙 t:Tmτ:Tyt₁:Tmh:<{ ⊢ t₁ ⦂ Nat }>ih:∀ (t' : Tm), t₁ ⟶ t' → <{ ⊢ t' ⦂ Nat }>t₁':Tmhs:t₁ ⟶ t₁'⊢ <{ ⊢ iszero t₁' ⦂ Bool }> All goals completed! 🐙
Exercise★★★(finish_preservation_informal) (Optional, Manually graded)

Complete the following informal proof.

Theorem: If ⊢ t ⦂ T and t ⟶ t', then ⊢ t' ⦂ T.

Proof: By induction on a derivation of ⊢ t ⦂ T.

  • If the last rule in the derivation is ite, then t = if t₁ then t₂ else t₃, with ⊢ t₁ ⦂ Bool, ⊢ t₂ ⦂ T and ⊢ t₃ ⦂ T.

    Inspecting the rules for the small-step reduction relation and remembering that t has the form if ..., we see that the only ones that could have been used to prove t ⟶ t' are ifTrue, ifFalse, or ifStep.

    • If the last rule was ifTrue, then t' = t₂. But we know that ⊢ t₂ ⦂ T, so we are done.

    • If the last rule was ifFalse, then t' = t₃. But we know that ⊢ t₃ ⦂ T, so we are done.

    • If the last rule was ifStep, then t' = if t₁' then t₂ else t₃, where t₁ ⟶ t₁'. We know ⊢ t₁ ⦂ Bool so, by the IH, ⊢ t₁' ⦂ Bool. The ite rule then gives us ⊢ if t₁' then t₂ else t₃ ⦂ T, as required.

- If the last rule in the derivation were `tru`, then `t = true`.
  However, `true` does not step to anything, so this case is vacuously
  true.

- Similarly, neither `fls` nor `zero` could be the final rule in the
  derivation.

- If the last rule in the derivation is `succ`, then `t = succ t₁` with
  `⊢ t₁ ⦂ Nat` and `T = Nat`.  The only rule which could have been used to
  show that `t` steps is `succStep`, in which case `t₁` steps to some
  `t₁'`.  So, by the IH, `⊢ t₁' ⦂ Nat`, and hence `t' = succ t₁'` also has
  type `Nat` by `succ`.

- If the last rule in the derivation is `pred`, then `t = pred t₁` with
  `⊢ t₁ ⦂ Nat`.  There are only three rules which could have been the last
  rule in the derivation of `pred t₁ ⟶ t'`.

  - If the last rule was `predZero`, then `t' = 0` which has type `Nat`.

  - If the last rule was `predSucc`, then `t₁ = succ t'`; by inversion
    on the fact that `⊢ t₁ ⦂ Nat` it follows that `⊢ t' ⦂ Nat` as well.

  - If the last rule was `predStep`, then `t₁` steps to some `t₁'`; by the
    IH `⊢ t₁' ⦂ Nat`, and so `pred t₁'` has type `Nat` as well by
    `pred`.

- If the last rule in the derivation is `isZero`, then `t = iszero t₁`
  with `⊢ t₁ ⦂ Nat` and `T = Bool`.  There are only three rules which
  could have been the last rule in the derivation of `iszero t₁ ⟶ t'`.

  - If the last rule was `isZeroZero`, then `t' = true` which has type
    `Bool`.

  - If the last rule was `isZeroSucc`, then `t' = false` which has type
    `Bool`.

  - If the last rule was `isZeroStep`, then `t₁` steps to some `t₁'`.  By
    the IH, `⊢ t₁' ⦂ Nat` as well, and hence `t' = iszero t₁'` has type
    `Bool` by `isZero`.
Exercise★★★(preservation_alternate_proof)

Now prove the same property again by induction on the evaluation derivation instead of on the typing derivation. Begin by carefully reading and thinking about the first few lines of the above proofs to make sure you understand what each one is doing. The set-up for this proof is similar, but not exactly the same.

theorem preservation' (t t' : Tm) (τ : Ty) (hT : <{ ⊢ t ⦂ τ }>) (he : t ⟶ t') : <{ ⊢ t' ⦂ τ }> := t:Tmt':Tmτ:TyhT:<{ ⊢ t ⦂ τ }>he:t ⟶ t'⊢ <{ ⊢ t' ⦂ τ }> solution! induction he generalizing τ with t:Tmt':Tmt₁:Tmt₂:Tmτ:TyhT:<{ ⊢ if true then t₁ else t₂ ⦂ τ }>⊢ <{ ⊢ t₁ ⦂ τ }> cases hT with t:Tmt':Tmt₁:Tmt₂:Tmτ:Tyh₁:<{ ⊢ true ⦂ Bool }>h₂:<{ ⊢ t₁ ⦂ τ }>h₃:<{ ⊢ t₂ ⦂ τ }>⊢ <{ ⊢ t₁ ⦂ τ }> All goals completed! 🐙 t:Tmt':Tmt₁:Tmt₂:Tmτ:TyhT:<{ ⊢ if false then t₁ else t₂ ⦂ τ }>⊢ <{ ⊢ t₂ ⦂ τ }> cases hT with t:Tmt':Tmt₁:Tmt₂:Tmτ:Tyh₁:<{ ⊢ false ⦂ Bool }>h₂:<{ ⊢ t₁ ⦂ τ }>h₃:<{ ⊢ t₂ ⦂ τ }>⊢ <{ ⊢ t₂ ⦂ τ }> All goals completed! 🐙 t:Tmt':Tmc:Tmc':Tmt₂:Tmt₃:Tmhc:c ⟶ c'ih:∀ (τ : Ty), <{ ⊢ c ⦂ τ }> → <{ ⊢ c' ⦂ τ }>τ:TyhT:<{ ⊢ if c then t₂ else t₃ ⦂ τ }>⊢ <{ ⊢ if c' then t₂ else t₃ ⦂ τ }> cases hT with t:Tmt':Tmc:Tmc':Tmt₂:Tmt₃:Tmhc:c ⟶ c'ih:∀ (τ : Ty), <{ ⊢ c ⦂ τ }> → <{ ⊢ c' ⦂ τ }>τ:Tyh₁:<{ ⊢ c ⦂ Bool }>h₂:<{ ⊢ t₂ ⦂ τ }>h₃:<{ ⊢ t₃ ⦂ τ }>⊢ <{ ⊢ if c' then t₂ else t₃ ⦂ τ }> All goals completed! 🐙 t:Tmt':Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (τ : Ty), <{ ⊢ t₁ ⦂ τ }> → <{ ⊢ t₁' ⦂ τ }>τ:TyhT:<{ ⊢ succ t₁ ⦂ τ }>⊢ <{ ⊢ succ t₁' ⦂ τ }> cases hT with t:Tmt':Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (τ : Ty), <{ ⊢ t₁ ⦂ τ }> → <{ ⊢ t₁' ⦂ τ }>h:<{ ⊢ t₁ ⦂ Nat }>⊢ <{ ⊢ succ t₁' ⦂ Nat }> All goals completed! 🐙 t:Tmt':Tmτ:TyhT:<{ ⊢ pred 0 ⦂ τ }>⊢ <{ ⊢ 0 ⦂ τ }> cases hT with t:Tmt':Tmh:<{ ⊢ 0 ⦂ Nat }>⊢ <{ ⊢ 0 ⦂ Nat }> All goals completed! 🐙 t:Tmt':Tmv:Tmhv:v.IsNValueτ:TyhT:<{ ⊢ pred (succ v) ⦂ τ }>⊢ <{ ⊢ v ⦂ τ }> cases hT with t:Tmt':Tmv:Tmhv:v.IsNValueh:<{ ⊢ succ v ⦂ Nat }>⊢ <{ ⊢ v ⦂ Nat }> cases h with t:Tmt':Tmv:Tmhv:v.IsNValuehh:<{ ⊢ v ⦂ Nat }>⊢ <{ ⊢ v ⦂ Nat }> All goals completed! 🐙 t:Tmt':Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (τ : Ty), <{ ⊢ t₁ ⦂ τ }> → <{ ⊢ t₁' ⦂ τ }>τ:TyhT:<{ ⊢ pred t₁ ⦂ τ }>⊢ <{ ⊢ pred t₁' ⦂ τ }> cases hT with t:Tmt':Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (τ : Ty), <{ ⊢ t₁ ⦂ τ }> → <{ ⊢ t₁' ⦂ τ }>h:<{ ⊢ t₁ ⦂ Nat }>⊢ <{ ⊢ pred t₁' ⦂ Nat }> All goals completed! 🐙 t:Tmt':Tmτ:TyhT:<{ ⊢ iszero 0 ⦂ τ }>⊢ <{ ⊢ true ⦂ τ }> cases hT with t:Tmt':Tmh:<{ ⊢ 0 ⦂ Nat }>⊢ <{ ⊢ true ⦂ Bool }> All goals completed! 🐙 t:Tmt':Tmv:Tmhv:v.IsNValueτ:TyhT:<{ ⊢ iszero (succ v) ⦂ τ }>⊢ <{ ⊢ false ⦂ τ }> cases hT with t:Tmt':Tmv:Tmhv:v.IsNValueh:<{ ⊢ succ v ⦂ Nat }>⊢ <{ ⊢ false ⦂ Bool }> All goals completed! 🐙 t:Tmt':Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (τ : Ty), <{ ⊢ t₁ ⦂ τ }> → <{ ⊢ t₁' ⦂ τ }>τ:TyhT:<{ ⊢ iszero t₁ ⦂ τ }>⊢ <{ ⊢ iszero t₁' ⦂ τ }> cases hT with t:Tmt':Tmt₁:Tmt₁':Tmhs:t₁ ⟶ t₁'ih:∀ (τ : Ty), <{ ⊢ t₁ ⦂ τ }> → <{ ⊢ t₁' ⦂ τ }>h:<{ ⊢ t₁ ⦂ Nat }>⊢ <{ ⊢ iszero t₁' ⦂ Bool }> All goals completed! 🐙

The preservation theorem is often called subject reduction, because it tells us what happens when the "subject" of the typing relation is reduced. This terminology comes from thinking of typing statements as sentences, where the term is the subject and the type is the predicate.

4.1.8. Type Soundness🔗

Putting progress and preservation together, we see that a well-typed term can never reach a stuck state.

def Tm.MultiStep (t₁ t₂ : Tm) : Prop := Multi Tm.Step t₁ t₂ scoped notation:40 t₁:41 " ⟶* " t₂:41 => Tm.MultiStep t₁ t₂ theorem soundness (t t' : Tm) (τ : Ty) (hT : <{ ⊢ t ⦂ τ }>) (hm : t ⟶* t') : ¬ Tm.IsStuck t' := t:Tmt':Tmτ:TyhT:<{ ⊢ t ⦂ τ }>hm:t ⟶* t'⊢ ¬t'.IsStuck induction hm generalizing τ with t:Tmt':Tma:Tmτ:TyhT:<{ ⊢ a ⦂ τ }>⊢ ¬a.IsStuck t:Tmt':Tma:Tmτ:TyhT:<{ ⊢ a ⦂ τ }>hst:a.IsStuck⊢ False; t:Tmt':Tma:Tmτ:TyhT:<{ ⊢ a ⦂ τ }>hnf:a.IsNormalFormhnv:¬a.IsValue⊢ False cases progress a τ hT with t:Tmt':Tma:Tmτ:TyhT:<{ ⊢ a ⦂ τ }>hnf:a.IsNormalFormhnv:¬a.IsValuehv:a.IsValue⊢ False All goals completed! 🐙 t:Tmt':Tma:Tmτ:TyhT:<{ ⊢ a ⦂ τ }>hnf:a.IsNormalFormhnv:¬a.IsValuehs:∃ t', a ⟶ t'⊢ False All goals completed! 🐙 t:Tmt':Tma:Tmb:Tmc:Tmh₁:a ⟶ bh₂:Multi Tm.Step b cih:∀ (τ : Ty), <{ ⊢ b ⦂ τ }> → ¬c.IsStuckτ:TyhT:<{ ⊢ a ⦂ τ }>⊢ ¬c.IsStuck All goals completed! 🐙
Quiz

Suppose we add the following two new rules to the reduction relation:

| predTrue  : pred true  ⟶ pred false
| predFalse : pred false ⟶ pred true

Which of the following properties remain true in the presence of these rules? (Choose 1 for yes, 2 for no.)

  • Determinism of Tm.Step

  • Progress

  • Preservation

Show solution

All three remain true.

Quiz

Suppose, instead, that we add this new rule to the typing relation:

| ifFunny : ⊢ t₂ ⦂ Nat → ⊢ if true then t₂ else t₃ ⦂ Nat

Which of the following properties remain true in the presence of this rule?

  • Determinism of Tm.Step

  • Progress

  • Preservation

Show solution

All three remain true.

4.2. Additional Exercises🔗

Exercise★★★(subject_expansion)

Having seen the subject reduction property, one might wonder whether the opposite property — subject expansion — also holds. That is, is it always the case that, if t ⟶ t' and ⊢ t' ⦂ T, then ⊢ t ⦂ T? If so, prove it. If not, give a counter-example.

Subject expansion does not hold in this language (or most interesting
languages).  For example, `if false then true else 0` is ill typed, but
it reduces to the well-typed term `0`.
theorem subject_expansion : (∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }>) ∨ ¬ (∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }>) := ⊢ (∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }>) ∨ ¬∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }> solution! ⊢ ¬∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }> hse:∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }>⊢ False hse:∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }>hT:<{ ⊢ if false then true else 0 ⦂ Nat }>⊢ False cases hT with hse:∀ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ⊢ t' ⦂ τ }> → <{ ⊢ t ⦂ τ }>h₁:<{ ⊢ false ⦂ Bool }>h₂:<{ ⊢ true ⦂ Nat }>h₃:<{ ⊢ 0 ⦂ Nat }>⊢ False All goals completed! 🐙 end TM

The following are thought exercises: for each modification, say which of determinism / progress / preservation still hold, with a counterexample if one breaks. (These are graded manually; there is no Lean code to complete.)

Note to developers
HIDE: Two further variations kept for the instructors only (they overlap
with the two quizzes in the Type Soundness section above).

variation1a (EX2M?): add the two step rules
  predTrue  : pred true  ⟶ pred false
  predFalse : pred false ⟶ pred true
-- Determinism, Progress, and Preservation all remain true.

variation1b (EX2M?): add the typing rule
  ifFunny : ⊢ t₂ ⦂ Nat → ⊢ if true then t₂ else t₃ ⦂ Nat
-- Determinism, Progress, and Preservation all remain true.
Exercise★★(variation1) (Manually graded)

Suppose that we add this new rule to the typing relation:

succBool : ⊢ t ⦂ Bool → ⊢ succ t ⦂ Bool

Which of the following properties remain true in the presence of this rule? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample.

  • Determinism of Tm.Step

  • Progress

  • Preservation

- Determinism: remains true (the `step` relation is unchanged).
- Progress: becomes false -- `succ true` is now well typed (`⊢ succ true ⦂
  Bool`) but is stuck.
- Preservation: remains true.
Exercise★★(variation2) (Manually graded)

Suppose, instead, that we add this new rule to the Tm.Step relation:

funny1 : if true then t₂ else t₃ ⟶ t₃

Which of the above properties become false in the presence of this rule? For each one that does, give a counter-example.

- Determinism: becomes false -- `if true then 0 else (succ 0)` can now step
  to either `0` (ifTrue) or `succ 0` (funny1).
- Progress and preservation: remain true.
Exercise★★(variation3) (Optional)

Suppose instead that we add this rule:

funny2 : t₂ ⟶ t₂' → if t₁ then t₂ else t₃ ⟶ if t₁ then t₂' else t₃

Which of the above properties become false in the presence of this rule? For each one that does, give a counter-example.

Determinism becomes false (e.g. `if false then (pred 0) else (succ 0)`
can step by either `ifFalse` or the new rule).  Progress and
preservation remain true.
Exercise★★(variation4) (Optional)

Suppose instead that we add this rule:

funny3 : pred false ⟶ pred (pred false)

Which of the above properties become false in the presence of this rule? For each one that does, give a counter-example.

All three properties remain true.
Exercise★★(variation5) (Optional)

Suppose instead that we add this rule:

funny4 : ⊢ 0 ⦂ Bool

Which of the above properties become false in the presence of this rule? For each one that does, give a counter-example.

Progress becomes false: `if 0 then true else true` has type `Bool`, is a
   normal form, and is not a value.
Exercise★★(variation6) (Optional)

Suppose instead that we add this rule:

funny5 : ⊢ pred 0 ⦂ Bool

Which of the above properties become false in the presence of this rule? For each one that does, give a counter-example.

Preservation becomes false: `pred 0` has type `Bool` and steps to `0`,
   which does not have type `Bool`.
Exercise★★★(more_variations) (Optional)

Make up some exercises of your own along the same lines as the ones above. Try to find ways of selectively breaking properties — i.e., ways of changing the definitions that break just one of the properties and leave the others alone.

Exercise★(remove_pred0) (Manually graded)

The reduction rule predZero is a bit counter-intuitive: we might feel that it makes more sense for the predecessor of 0 to be undefined, rather than being defined to be 0. Can we achieve this simply by removing the rule from the definition of Tm.Step? Would doing so create any problems elsewhere?

Yes, but doing this would break the progress property.  A better way would
be to raise an exception in this case, but this requires that we add
exceptions to the language we're formalizing!
Exercise★★★★(prog_pres_bigstep) (Advanced, Manually graded)

Suppose our evaluation relation is defined in the big-step style. State appropriate analogs of the progress and preservation properties. (You do not need to prove them.)

Can you see any limitations of either of your properties? Do they allow for nonterminating programs? Why might we prefer the small-step semantics for stating preservation and progress?

The type preservation property for the big-step semantics is similar to
the one we gave for the small-step semantics: if a well-typed term
evaluates to some final value, then this value has the same type as the
original term.  The proof is similar to the one we gave.  However,
preservation for small-step semantics implies that all intermediate states
(i.e., all states reachable in multi-step) are well-typed, whereas big-step
semantics only relates a term to its final evaluation result, with no
notion of "intermediate state" about which preservation can make
guarantees.

The situation with the progress property is more interesting.  A direct
analog (if a term is well typed then it evaluates to some other term)
makes a much stronger claim than the progress theorem we have given: it
says that every well-typed term can be evaluated to some final value---that
is, that evaluation always terminates on well-typed terms.  For arithmetic
expressions, this happens to be the case, but for more interesting
languages (languages involving general recursion, for example) it will
often not be true.  For such languages, we simply have no progress property
in the big-step style: in effect, there is no way to tell the difference
between reaching an error state and failing to terminate.  This is one
reason that language theorists generally prefer the small-step style.
Note to developers (Benjamin Pierce @bcpierce00)

This next is not using the new conventions for grade blocks, which I thought to_verso.py was now enforcing. Is that because this file was converted a while back, before these improvements? (I suspect yes because the indentation is also wonky and I improved that too.) Anyway, the grade block headers should be fixed, throughout (and maybe in Smallstep and Imp?)... dev block headers too, if we want to be really consistent.

Source revision: e85fe77, committed 2026-10-06 21:16 UTC