Type Systems

6. StlcProp: Properties of STLC🔗

THE SIMPLY TYPED LAMBDA CALCULUS

Syntax:

t::=x(variable)
|λ x : τ . t(abstraction)
|t t(application)
|true(constant true)
|false(constant false)
|if t then t else t(conditional)

Values:

v::=λ x : τ . t
|true
|false

Substitution:

[x:=s]x               = s
[x:=s]y               = y                     if x ≠ y
[x:=s](λx:τ. t)       = λx:τ. t
[x:=s](λy:τ. t)       = λy:τ. [x:=s]t         if x ≠ y
[x:=s](t₁ t₂)         = ([x:=s]t₁) ([x:=s]t₂)
[x:=s]true            = true
[x:=s]false           = false
[x:=s](if t₁ then t₂ else t₃) =
                if [x:=s]t₁ then [x:=s]t₂ else [x:=s]t₃

Small-step operational semantics:

                              v.IsValue
                       -----------------------                    (appAbs)
                        (λx:τ. t) v ⟶ [x:=v]t

                              t₁ ⟶ t₁'
                          ----------------                        (app1)
                           t₁ t₂ ⟶ t₁' t₂

                             v₁.IsValue
                              t₂ ⟶ t₂'
                          ----------------                        (app2)
                           v₁ t₂ ⟶ v₁ t₂'

                  --------------------------------                (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₃)

Typing:

                              Γ x = τ₁
                            ------------                       (var)
                             Γ ⊢ x ⦂ τ₁

                        x ↦ τ₂ ; Γ ⊢ t₁ ⦂ τ₁
                      -------------------------                (abs)
                       Γ ⊢ λx:τ₂. t₁ ⦂ τ₂ → τ₁

                          Γ ⊢ t₁ ⦂ τ₂ → τ₁
                            Γ ⊢ t₂ ⦂ τ₂
                         ------------------                    (app)
                           Γ ⊢ t₁ t₂ ⦂ τ₁

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

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

             Γ ⊢ t₁ ⦂ Bool    Γ ⊢ t₂ ⦂ τ₁    Γ ⊢ t₃ ⦂ τ₁
            ---------------------------------------------      (ite)
                   Γ ⊢ if t₁ then t₂ else t₃ ⦂ τ₁
Note to developers (Benjamin Pierce @bcpierce00, before next release, 2022)

In Wadler's "PLF in Agda", he defines an "animator" for STLC terms using the proof terms for progress + preservation. This would be a FANTASTIC example (or, perhaps better, exercise!) for this chapter.

In this chapter, we develop the fundamental theory of the Simply Typed Lambda Calculus — in particular, the type safety theorem.

We pick up where the Stlc chapter left off, so everything below lives in the same namespace as the definitions it is about.

namespace Stlc open scoped MyGetElem open scoped Elab

6.1. Canonical Forms🔗

Formally, we will need these lemmas only for terms that are not only well typed but closed — i.e., well typed in the empty context.

theorem canonical_forms_bool (t : Tm) (hτ : <{ ∅ ⊢ t ⦂ Bool }>) (hv : t.IsValue) : t = <{ true }> ∨ t = <{ false }> := t:Tmhτ:<{ ∅ ⊢ t ⦂ Bool }>hv:t.IsValue⊢ t = <{ true }> ∨ t = <{ false }> cases hv with x:Stringτ:Tyt₁:Tmhτ:<{ ∅ ⊢ λ ~x : τ . t₁ ⦂ Bool }>⊢ <{ λ ~x : τ . t₁ }> = <{ true }> ∨ <{ λ ~x : τ . t₁ }> = <{ false }> All goals completed! 🐙 hτ:<{ ∅ ⊢ true ⦂ Bool }>⊢ <{ true }> = <{ true }> ∨ <{ true }> = <{ false }> hτ:<{ ∅ ⊢ true ⦂ Bool }>⊢ <{ true }> = <{ true }>; All goals completed! 🐙 hτ:<{ ∅ ⊢ false ⦂ Bool }>⊢ <{ false }> = <{ true }> ∨ <{ false }> = <{ false }> hτ:<{ ∅ ⊢ false ⦂ Bool }>⊢ <{ false }> = <{ false }>; All goals completed! 🐙 theorem canonical_forms_fun (t : Tm) (τ₁ τ₂ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ₁ → τ₂ }>) (hv : t.IsValue) : ∃ x u, t = <{ λ x : τ₁ . u }> := t:Tmτ₁:Tyτ₂:Tyhτ:<{ ∅ ⊢ t ⦂ τ₁ → τ₂ }>hv:t.IsValue⊢ ∃ x u, t = <{ λ ~x : τ₁ . u }> cases hv with τ₁:Tyτ₂:Tyx:Stringτ:Tyt₁:Tmhτ:<{ ∅ ⊢ λ ~x : τ . t₁ ⦂ τ₁ → τ₂ }>⊢ ∃ x_1 u, <{ λ ~x : τ . t₁ }> = <{ λ ~x_1 : τ₁ . u }> cases hτ with τ₁:Tyτ₂:Tyx:Stringt₁:Tmh✝:<{ ~(x →ₚ τ₁) ⊢ t₁ ⦂ τ₂ }>⊢ ∃ x_1 u, <{ λ ~x : τ₁ . t₁ }> = <{ λ ~x_1 : τ₁ . u }> All goals completed! 🐙 τ₁:Tyτ₂:Tyhτ:<{ ∅ ⊢ true ⦂ τ₁ → τ₂ }>⊢ ∃ x u, <{ true }> = <{ λ ~x : τ₁ . u }> All goals completed! 🐙 τ₁:Tyτ₂:Tyhτ:<{ ∅ ⊢ false ⦂ τ₁ → τ₂ }>⊢ ∃ x u, <{ false }> = <{ λ ~x : τ₁ . u }> All goals completed! 🐙

6.2. Progress🔗

The progress theorem tells us that closed, well-typed terms are not stuck.

theorem progress (t : Tm) (τ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ }>) : t.IsValue ∨ ∃ t', t ⟶ t' := t:Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t' t:Tmτ:TyΓ:ContexthΓ:∅ = Γhτ:<{ Γ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t' induction hτ with t:Tmτ:TyΓ✝:ContextΓ:Contextx:Stringτ₁:Tyh:Γ[x] = some τ₁hΓ:∅ = Γ⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t' t:Tmτ:TyΓ:Contextx:Stringτ₁:Tyh:∅[x] = some τ₁⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t' -- Contradictory: variables cannot be typed in an empty context. t:Tmτ:TyΓ:Contextx:Stringτ₁:Tyh:none = some τ₁⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t' All goals completed! 🐙 t:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>h_ih✝:∅ = x✝ →ₚ τ₂✝ ; Γ✝ → t₁✝.IsValue ∨ ∃ t', t₁✝ ⟶ t'hΓ:∅ = Γ✝⊢ <{ λ ~x✝ : τ₂✝ . t₁✝ }>.IsValue ∨ ∃ t', <{ λ ~x✝ : τ₂✝ . t₁✝ }> ⟶ t' t:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>h_ih✝:∅ = x✝ →ₚ τ₂✝ ; Γ✝ → t₁✝.IsValue ∨ ∃ t', t₁✝ ⟶ t'hΓ:∅ = Γ✝⊢ <{ λ ~x✝ : τ₂✝ . t₁✝ }>.IsValue; All goals completed! 🐙 t:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t' t:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ true }>.IsValue; All goals completed! 🐙 t:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t' t:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ false }>.IsValue; All goals completed! 🐙 t:Tmτ:TyΓ✝:ContextΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ Γ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ Γ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = Γ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = Γ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hΓ:∅ = Γ⊢ <{ t₁ t₂ }>.IsValue ∨ ∃ t', <{ t₁ t₂ }> ⟶ t' -- `t = t₁ t₂`. Proceed by cases on whether `t₁` is a value or steps. t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'⊢ <{ t₁ t₂ }>.IsValue ∨ ∃ t', <{ t₁ t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' cases ih₁ rfl with t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValue⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' cases ih₂ rfl with t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuehv₂:t₂.IsValue⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₂:t₂.IsValuex:Stringu:Tmh₁:<{ ∅ ⊢ λ ~x : τ₂ . u ⦂ τ₂ → τ₁ }>ih₁:∅ = ∅ → <{ λ ~x : τ₂ . u }>.IsValue ∨ ∃ t', <{ λ ~x : τ₂ . u }> ⟶ t'hv₁:<{ λ ~x : τ₂ . u }>.IsValue⊢ ∃ t', <{ (λ ~x : τ₂ . u) t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₂:t₂.IsValuex:Stringu:Tmh₁:<{ ∅ ⊢ λ ~x : τ₂ . u ⦂ τ₂ → τ₁ }>ih₁:∅ = ∅ → <{ λ ~x : τ₂ . u }>.IsValue ∨ ∃ t', <{ λ ~x : τ₂ . u }> ⟶ t'hv₁:<{ λ ~x : τ₂ . u }>.IsValue⊢ <{ (λ ~x : τ₂ . u) t₂ }> ⟶ <{ [~x := t₂] u }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₂:t₂.IsValuex:Stringu:Tmh₁:<{ ∅ ⊢ λ ~x : τ₂ . u ⦂ τ₂ → τ₁ }>ih₁:∅ = ∅ → <{ λ ~x : τ₂ . u }>.IsValue ∨ ∃ t', <{ λ ~x : τ₂ . u }> ⟶ t'hv₁:<{ λ ~x : τ₂ . u }>.IsValue⊢ t₂.IsValue All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuehs₂:∃ t', t₂ ⟶ t'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ <{ t₁ t₂ }> ⟶ <{ t₁ t₂' }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₁.IsValuet:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₁.IsValuet:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂' All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hs₁:∃ t', t₁ ⟶ t'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ <{ t₁ t₂ }> ⟶ <{ t₁' t₂ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' All goals completed! 🐙 t:Tmτ:TyΓ✝:ContextΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ Γ ⊢ t₁ ⦂ Bool }>h₂:<{ Γ ⊢ t₂ ⦂ τ₁ }>h₃:<{ Γ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = Γ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = Γ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = Γ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hΓ:∅ = Γ⊢ <{ if t₁ then t₂ else t₃ }>.IsValue ∨ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ 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τ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ 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₁ rfl with t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', 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 canonical_forms_bool t₁ h₁ hv₁ with t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hv₁:t₁.IsValuehe:t₁ = <{ true }>⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' t:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ true ⦂ Bool }>ih₁:∅ = ∅ → <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t'hv₁:<{ true }>.IsValue⊢ ∃ t', <{ if true then t₂ else t₃ }> ⟶ t' t:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ true ⦂ Bool }>ih₁:∅ = ∅ → <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t'hv₁:<{ true }>.IsValue⊢ <{ if true then t₂ else t₃ }> ⟶ t₂ All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hv₁:t₁.IsValuehe:t₁ = <{ false }>⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t' t:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ false ⦂ Bool }>ih₁:∅ = ∅ → <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t'hv₁:<{ false }>.IsValue⊢ ∃ t', <{ if false then t₂ else t₃ }> ⟶ t' t:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ false ⦂ Bool }>ih₁:∅ = ∅ → <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t'hv₁:<{ false }>.IsValue⊢ <{ if false then t₂ else t₃ }> ⟶ t₃ All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', 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τ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', 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' t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ <{ if t₁ then t₂ else t₃ }> ⟶ <{ if t₁' then t₂ else t₃ }> t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' All goals completed! 🐙

6.3. Preservation🔗

For preservation, we need some technical machinery for reasoning about variables and substitution.

  • The preservation theorem is proved by induction on a typing derivation and case analysis on the step relation, pretty much as we did in the Types chapter.

    Main novelty: Step.appAbs uses the substitution operation.

    To see that this step preserves typing, we need to know that the substitution itself does. So we prove a...

  • substitution lemma, stating that substituting a (closed, well-typed) term s for a variable x in a term t preserves the type of t.

The proof goes by induction on the form of t and requires looking at all the different cases in the definition of substitution.

Tricky case: variables.

In this case, we need to deduce from the fact that a term s has type σ in the empty context the fact that s has type σ in every context.

For this we prove a...

  • weakening lemma, showing that typing is preserved under "extensions" to the context Γ.

To make Lean happy, we need to formalize all this in the opposite order...

6.3.1. The Weakening Lemma🔗

First, we show that typing is preserved under "extensions" to the context Γ. (Recall map inclusion, Γ ⊆ Γ', from the Typeclasses chapter.)

theorem weakening {Γ Γ' : Context} {t : Tm} {τ : Ty} (hi : Γ ⊆ Γ') (ht : <{ Γ ⊢ t ⦂ τ }>) : <{ Γ' ⊢ t ⦂ τ }> := Γ:ContextΓ':Contextt:Tmτ:Tyhi:Γ ⊆ Γ'ht:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ' ⊢ t ⦂ τ }> induction ht generalizing Γ' with Γ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyh:Γ✝[x] = some τ₁✝Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ ~(Stlc.Tm.var x) ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyh:Γ✝[x] = some τ₁✝Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ'[x] = some τ₁✝ All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ λ ~x : τ₂✝ . t₁✝ ⦂ τ₂✝ → τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ ~(x →ₚ τ₂✝ ; Γ') ⊢ t₁✝ ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ x →ₚ τ₂✝ ; Γ✝ ⊆ x →ₚ τ₂✝ ; Γ' Γ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ' All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ t₂✝ ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ ~?app.τ₂ → τ₁✝ }>Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ ~?app.τ₂ }>Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Ty Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ ~?app.τ₂ → τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ' All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ' All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:ContextΓ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ true ⦂ Bool }> All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:ContextΓ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ false ⦂ Bool }> All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ if t₁✝ then t₂✝ else t₃✝ ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ Bool }>Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ Bool }> Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ' All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ' All goals completed! 🐙 Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }> Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ' All goals completed! 🐙

Through judicious use of apply_rules, we can heavily automate this proof. The tactic after with is applied to every case of the induction and handles all the cases using apply_rules's automation. We must give the tactic access to all the HasType constructors and the PartialMap.update_subset lemma for this to work:

theorem weakening' {Γ Γ' : Context} {t : Tm} {τ : Ty} (hi : Γ ⊆ Γ') (ht : <{ Γ ⊢ t ⦂ τ }>) : <{ Γ' ⊢ t ⦂ τ }> := Γ:ContextΓ':Contextt:Tmτ:Tyhi:Γ ⊆ Γ'ht:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ' ⊢ t ⦂ τ }> induction ht generalizing Γ' with (All goals completed! 🐙)

The following simple corollary is what we actually need below.

theorem weakening_empty {Γ : Context} {t : Tm} {τ : Ty} (ht : <{ ∅ ⊢ t ⦂ τ }>) : <{ Γ ⊢ t ⦂ τ }> := Γ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ <{ Γ ⊢ t ⦂ τ }> Γ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ ∅ ⊆ ΓΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ <{ ∅ ⊢ t ⦂ τ }> -- this is the "manual" way to show that the empty context is a subset of any context: -- show that a 'lookup' in it is impossible. Γ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ ∅ ⊆ Γ Γ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>x:Stringb:Tycontra:∅[x] = some b⊢ Γ[x] = some b All goals completed! 🐙 Γ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ <{ ∅ ⊢ t ⦂ τ }> All goals completed! 🐙

6.3.2. The Substitution Lemma🔗

Now we come to the conceptual heart of the proof that reduction preserves types — namely, the observation that substitution preserves types.

The substitution lemma says:

  • Suppose we have a term t with a free variable x, and suppose we've been able to assign a type τ to t under the assumption that x has some type τ'.

  • Also, suppose that we have some other term v and that we've shown that v has type τ'.

  • Then we can substitute v for each of the occurrences of x in t and obtain a new term that still has type τ.

theorem substitution_preserves_typing (Γ : Context) (x : String) (τ' : Ty) (t v : Tm) (τ : Ty) (hτ : <{ x ↦ τ' ; Γ ⊢ t ⦂ τ }>) (hv : <{ ∅ ⊢ v ⦂ τ' }>) : <{ Γ ⊢ [x := v] t ⦂ τ }> := Γ:Contextx:Stringτ':Tyt:Tmv:Tmτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>hv:<{ ∅ ⊢ v ⦂ τ' }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }> -- By induction on `t`; in each case we get at the derivation of `hτ`. induction t generalizing Γ τ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ ~(Stlc.Tm.var y) ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> cases hτ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[x] = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var x) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var x) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ <{ Γ ⊢ v ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τhτ'τ:τ' = τ⊢ <{ Γ ⊢ v ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contexth:some τ' = some τ'⊢ <{ Γ ⊢ v ⦂ τ' }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contexth:some τ' = some τ'⊢ <{ ∅ ⊢ v ⦂ τ' }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ ~(Stlc.Tm.var y) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ Γ[y] = some τ All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ t₂ ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (t₁ t₂) ⦂ τ }> cases hτ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] (t₁ t₂) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ [~x := v] t₂ ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ ⦂ ~?app.app.τ₂ → τ }>x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₂ ⦂ ~?app.app.τ₂ }>x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ Ty x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ ⦂ ~?app.app.τ₂ → τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ ~?app.app.τ₂ → τ }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₂ ⦂ τ₂✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ λ ~y : σ . t₁ ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ τ }> cases hτ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }>x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ [~x := v] (λ ~x : σ . t₁) ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ λ ~x : σ . t₁ ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ λ ~x : σ . t₁ ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ λ ~y : σ . [~x := v] t₁ ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ λ ~y : σ . [~x := v] t₁ ⦂ σ → τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ ~(y →ₚ σ ; Γ) ⊢ [~x := v] t₁ ⦂ τ₁✝ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ true ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] true ⦂ τ }> cases hτ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ [~x := v] true ⦂ Bool }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ true ⦂ Bool }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ false ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] false ⦂ τ }> cases hτ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ [~x := v] false ⦂ Bool }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ false ⦂ Bool }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ if c then t else e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (if c then t else e) ⦂ τ }> cases hτ with x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (if c then t else e) ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ if [~x := v] c then [~x := v] t else [~x := v] e ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] c ⦂ Bool }>x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }>x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] e ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] c ⦂ Bool }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> All goals completed! 🐙 x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] e ⦂ τ }> x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> All goals completed! 🐙

6.3.3. Main Theorem🔗

We now have the ingredients we need to prove preservation: if a closed, well-typed term t has type τ and takes a step to t', then t' is also a closed term with type τ. In other words, the small-step reduction relation preserves types.

theorem preservation (t t' : Tm) (τ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ }>) (hs : t ⟶ t') : <{ ∅ ⊢ t' ⦂ τ }> := t:Tmt':Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>hs:t ⟶ t'⊢ <{ ∅ ⊢ t' ⦂ τ }> t:Tmt':Tmτ:Tyhs:t ⟶ t'Γ:ContexthΓ:∅ = Γhτ:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ ⊢ t' ⦂ τ }> induction hτ generalizing t' with t:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyh✝:Γ✝[x✝] = some τ₁✝t':Tmhs:Stlc.Tm.var x✝ ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ τ₁✝ }> All goals completed! 🐙 t:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>h_ih✝:∀ (t' : Tm), t₁✝ ⟶ t' → ∅ = x✝ →ₚ τ₂✝ ; Γ✝ → <{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t' ⦂ τ₁✝ }>t':Tmhs:<{ λ ~x✝ : τ₂✝ . t₁✝ }> ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ τ₂✝ → τ₁✝ }> All goals completed! 🐙 t:Tmτ:TyΓ:ContextΓ✝:Contextt':Tmhs:<{ true }> ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ Bool }> All goals completed! 🐙 t:Tmτ:TyΓ:ContextΓ✝:Contextt':Tmhs:<{ false }> ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ Bool }> All goals completed! 🐙 t:Tmτ:TyΓ✝:ContextΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ Γ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ Γ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₂ }>t':Tmhs:<{ t₁ t₂ }> ⟶ t'hΓ:∅ = Γ⊢ <{ Γ ⊢ t' ⦂ τ₁ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmt':Tmhs:<{ t₁ t₂ }> ⟶ t'h₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>⊢ <{ ∅ ⊢ t' ⦂ τ₁ }> cases hs with t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringτ✝:Tyt✝:Tmh₁:<{ ∅ ⊢ λ ~x✝ : τ✝ . t✝ ⦂ τ₂ → τ₁ }>ih₁:∀ (t' : Tm), <{ λ ~x✝ : τ✝ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hv✝:t₂.IsValue⊢ <{ ∅ ⊢ [~x✝ := t₂] t✝ ⦂ τ₁ }> -- The one interesting case: the desired result is the substitution lemma. cases h₁ with t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ∅ ⊢ [~x✝ := t₂] t✝ ⦂ τ₁ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ~(x✝ →ₚ ?app.appAbs.abs.τ') ⊢ t✝ ⦂ τ₁ }>t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ∅ ⊢ t₂ ⦂ ~?app.appAbs.abs.τ' }>t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ Ty t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ~(x✝ →ₚ ?app.appAbs.abs.τ') ⊢ t✝ ⦂ τ₁ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ∅ ⊢ t₂ ⦂ τ₂ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' t₂ ⦂ τ₁ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ ~?app.app1.τ₂ → τ₁ }>t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ ~?app.app1.τ₂ }>t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ Ty t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ ~?app.app1.τ₂ → τ₁ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁'t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅ t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅ All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ τ₂ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₁ t₂' ⦂ τ₁ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₁ ⦂ ~?app.app2.τ₂ → τ₁ }>t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₂' ⦂ ~?app.app2.τ₂ }>t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ Ty t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₁ ⦂ ~?app.app2.τ₂ → τ₁ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₂' ⦂ τ₂ }> t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂'t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ ∅ = ∅ t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂' All goals completed! 🐙 t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ ∅ = ∅ All goals completed! 🐙 t:Tmτ:TyΓ✝:ContextΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ Γ ⊢ t₁ ⦂ Bool }>h₂:<{ Γ ⊢ t₂ ⦂ τ₁ }>h₃:<{ Γ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₁ }>t':Tmhs:<{ if t₁ then t₂ else t₃ }> ⟶ t'hΓ:∅ = Γ⊢ <{ Γ ⊢ t' ⦂ τ₁ }> t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyt':Tmhs:<{ if t₁ then t₂ else t₃ }> ⟶ t'h₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>⊢ <{ ∅ ⊢ t' ⦂ τ₁ }> cases hs with t:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>h₁:<{ ∅ ⊢ true ⦂ Bool }>ih₁:∀ (t' : Tm), <{ true }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>⊢ <{ ∅ ⊢ t₂ ⦂ τ₁ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>h₁:<{ ∅ ⊢ false ⦂ Bool }>ih₁:∀ (t' : Tm), <{ false }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>⊢ <{ ∅ ⊢ t₃ ⦂ τ₁ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ if t₁' then t₂ else t₃ ⦂ τ₁ }> t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ Bool }>t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ τ₁ }>t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₃ ⦂ τ₁ }> t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ Bool }> t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁'t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅ t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅ All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ τ₁ }> All goals completed! 🐙 t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₃ ⦂ τ₁ }> All goals completed! 🐙

6.4. Type Soundness🔗

6.5. Uniqueness of Types🔗

6.6. Context Invariance (Optional)🔗

6.7. Additional Exercises🔗

The STLC typing relation with the funnyAbs rule of stlc_variation7 added, and a proof that progress then fails.

end Stlc

6.7.1. Exercise: STLC with Arithmetic🔗

Let's extend the STLC with a base type of numbers, some constants, and some primitive operators.

namespace StlcArith open scoped MyGetElem

To types, we add a base type of natural numbers (and remove booleans, for brevity).

inductive Ty where | arrow (τ₁ τ₂ : Ty) | nat

To terms, we add natural number constants, along with successor, predecessor, multiplication, and zero-testing.

inductive Tm where | var (x : String) | app (t₁ t₂ : Tm) | abs (x : String) (τ : Ty) (t : Tm) | const (n : Nat) | succ (t : Tm) | pred (t : Tm) | mult (t₁ t₂ : Tm) | ite0 (c t e : Tm)
Notation encodingscoped syntax:max num : stlcTm scoped syntax:60 stlcTm:60 " * " stlcTm:61 : stlcTm scoped syntax:50 "if0 " stlcTm:51 " then " stlcTm:50 " else " stlcTm:50 : stlcTm namespace Elab open StlcCommon open Lean Meta Elab Term def language : Language where tyType := ``Ty tmType := ``Tm arrowCtor := ``Ty.arrow varCtor := ``Tm.var appCtor := ``Tm.app absCtor := ``Tm.abs -- defined later subst := `StlcArith.subst hasType := `StlcArith.HasType def natTyHandler : TyElabHandler := fun _recur k T => do match T with | `(stlcTy| Nat) => return mkConst ``Ty.nat | _ => k T def tyHandlers : TyElabHandler := natTyHandler.orElse (commonTyHandler language) partial def elabTy : TyElab := tyHandlers elabTy <| unsupportedTy language def arithTmHandler : TmElabHandler := fun recur k Γ free t => do match t with | `(stlcTm| $n:num) => do return (mkApp (mkConst ``Tm.const) (mkNatLit n.getNat), free) | `(stlcTm| Nat) => do throwError "`Nat` is not a valid term." | `(stlcTm| succ $e:stlcTm) => do let (e, free) ← recur Γ free e return (mkApp (mkConst ``Tm.succ) e, free) | `(stlcTm| pred $e:stlcTm) => do let (e, free) ← recur Γ free e return (mkApp (mkConst ``Tm.pred) e, free) | `(stlcTm| $t₁:stlcTm * $t₂:stlcTm) => do let (e₁, free) ← recur Γ free t₁ let (e₂, free) ← recur Γ free t₂ return (mkApp2 (mkConst ``Tm.mult) e₁ e₂, free) | `(stlcTm| if0 $c:stlcTm then $t:stlcTm else $e:stlcTm) => do let (c, free) ← recur Γ free c let (t, free) ← recur Γ free t let (e, free) ← recur Γ free e return (mkApp3 (mkConst ``Tm.ite0) c t e, free) | _ => k Γ free t def tmHandlers : TmElabHandler := arithTmHandler.orElse (commonTmHandler language elabTy) partial def elabTm : TmElab := tmHandlers elabTm unsupportedTm def elabCtx : CtxElab := elabCtxCommon language elabTy @[scoped term_elab StlcCommon.bracket] def elabBracket : TermElab := fun stx expectedType? => do let `(<{ $q:stlcQuoted }>) := stx | throwUnsupportedSyntax elabQuoted language elabTy elabTm elabCtx q expectedType? end Elab open scoped Elab namespace Delab open StlcCommon Elab Delab open Lean PrettyPrinter Delaborator @[app_unexpander Ty.nat] private def Ty.unexpandNat : Unexpander | stx => do let T ← `(stlcTy| $(mkIdentFrom stx `Nat):ident) `(<{ $T:stlcTy }>) @[app_unexpander Ty.arrow] private def Ty.unexpandArrow : Unexpander := Delab.unexpandArrow private def reservedNames : String → Bool | "Nat" | "succ" | "pred" | "if0" => true | _ => false @[app_unexpander Tm.var] private def Tm.unexpandVar : Unexpander := Delab.unexpandVar reservedNames ``Tm.var @[app_delab Tm.var] private def Tm.delabVar : Delab := Delab.delabVar ``Tm.var @[app_unexpander Tm.app] private def Tm.unexpandApp : Unexpander := Delab.unexpandApp @[app_unexpander Tm.abs] private def Tm.unexpandAbs : Unexpander := Delab.unexpandAbs @[app_unexpander Tm.ite0] private def Tm.unexpandIte : Unexpander | `($_ $c $t $e) => `(<{ if0 $(getTm c) then $(getTm t) else $(getTm e) }>) | _ => throw () @[app_unexpander Tm.const] def Tm.unexpandConst : Unexpander | `($_ $n:num) => `(<{ $n:num }>) | _ => throw () @[app_unexpander Tm.succ] def Tm.unexpandSucc : Unexpander | stx@`($_ $t) => do let succ := mkObjectIdentFrom stx "succ" `(<{ $succ:ident $(getTm t) }>) | _ => throw () @[app_unexpander Tm.pred] def Tm.unexpandPred : Unexpander | stx@`($_ $t) => do let pred := mkObjectIdentFrom stx "pred" `(<{ $pred:ident $(getTm t) }>) | _ => throw () @[app_unexpander Tm.mult] def Tm.unexpandMult : Unexpander | `($_ $t₁ $t₂) => do let t ← `(stlcTm| $(getTm t₁) * $(getTm t₂)) let q ← `(stlcQuoted| $t:stlcTm) `(<{ $q:stlcQuoted }>) | _ => throw () end Delab

6.7.1.1. The Technical Theorems🔗

6.7.1.2. Preservation🔗

6.7.1.3. Progress🔗

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