5. Subject Reduction and Normal Forms🔗

import LeanLambda.SimplyTyped.Typingnamespace SimplyTypedopen Untypednamespace DB

5.1. Subject Reduction and Normal Forms🔗

This chapter studies the genuinely type-dependent facts about reduction and normal forms.

Preservation: reduction does not change the type of a term.
Representation: typing restricts the possible shapes of normal terms.

Weakening and substitution are supporting lemmas needed for preservation. The exhaustive and exclusive relationship between reduction and normality was already established for untyped terms and does not need to be repeated here.

5.1.1. Structural Lemmas🔗

5.1.1.1. Weakening🔗

Inserting a type into the bound context shifts precisely the indices at or above the insertion point. This is the typing form of weakening.

\frac{\Delta_1,\Delta_2;\Gamma \vdash e : A} {\Delta_1,C,\Delta_2;\Gamma \vdash \uparrow_{|\Delta_1|}e : A}

theorem typing_shift
  (ht : left ++ right ; Γ ⊢ᴺᵇ t : A)
  : left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove left.length t : A
:= byleft:BoundContextright:BoundContextΓ:FreeContextt:DBA:TyC:Tyht:left ++ right ; Γ ⊢ᴺᵇ t : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) t : A
  induction t generalizing left right AboundΓ:FreeContextC:Tyindex✝:ℕleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ DB.bound index✝ : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (DB.bound index✝) : AfreeΓ:FreeContextC:Tyx✝:Stringleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ DB.free x✝ : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (DB.free x✝) : AlamΓ:FreeContextC:Tybody✝:DBbody_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ body✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) body✝ : Aleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ body✝.lam : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) body✝.lam : AappΓ:FreeContextC:Tyfn✝:DBarg✝:DBfn_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ fn✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) fn✝ : Aarg_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) arg✝ : Aleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ fn✝.app arg✝ : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (fn✝.app arg✝) : A <;>boundΓ:FreeContextC:Tyindex✝:ℕleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ DB.bound index✝ : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (DB.bound index✝) : AfreeΓ:FreeContextC:Tyx✝:Stringleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ DB.free x✝ : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (DB.free x✝) : AlamΓ:FreeContextC:Tybody✝:DBbody_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ body✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) body✝ : Aleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ body✝.lam : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) body✝.lam : AappΓ:FreeContextC:Tyfn✝:DBarg✝:DBfn_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ fn✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) fn✝ : Aarg_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) arg✝ : Aleft:BoundContextright:BoundContextA:Tyht:left ++ right ; Γ ⊢ᴺᵇ fn✝.app arg✝ : A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (fn✝.app arg✝) : A
  cases htapp.appΓ:FreeContextC:Tyfn✝:DBarg✝:DBfn_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ fn✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) fn✝ : Aarg_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) arg✝ : Aleft:BoundContextright:BoundContextA:TyA✝:Tya✝¹:left ++ right ; Γ ⊢ᴺᵇ arg✝ : A✝a✝:left ++ right ; Γ ⊢ᴺᵇ fn✝ : A✝ ⇒ A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (fn✝.app arg✝) : A <;>bound.boundΓ:FreeContextC:Tyindex✝:ℕleft:BoundContextright:BoundContextA:Tya✝:(left ++ right)[index✝]? = some A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (DB.bound index✝) : Afree.freeΓ:FreeContextC:Tyx✝:Stringleft:BoundContextright:BoundContextA:Tya✝:List.lookup x✝ Γ = some A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (DB.free x✝) : Alam.lamΓ:FreeContextC:Tybody✝:DBbody_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ body✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) body✝ : Aleft:BoundContextright:BoundContextA✝:TyB✝:Tya✝:A✝ :: (left ++ right) ; Γ ⊢ᴺᵇ body✝ : B✝⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) body✝.lam : A✝ ⇒ B✝app.appΓ:FreeContextC:Tyfn✝:DBarg✝:DBfn_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ fn✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) fn✝ : Aarg_ih✝:∀ {left right : BoundContext} {A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg✝ : A) → left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) arg✝ : Aleft:BoundContextright:BoundContextA:TyA✝:Tya✝¹:left ++ right ; Γ ⊢ᴺᵇ arg✝ : A✝a✝:left ++ right ; Γ ⊢ᴺᵇ fn✝ : A✝ ⇒ A⊢ left ++ C :: right ; Γ ⊢ᴺᵇ DB.shiftAbove (List.length left) (fn✝.app arg✝) : A grind [DB.shiftAbove, DB.shiftRenaming, DB.HasType.app]All goals completed! 🐙

@[grind .] theorem typing_shift_head
  (ht : Δ ; Γ ⊢ᴺᵇ t : A)
  : C :: Δ ; Γ ⊢ᴺᵇ DB.shiftAbove 0 t : A
:= byΔ:BoundContextΓ:FreeContextt:DBA:TyC:Tyht:Δ ; Γ ⊢ᴺᵇ t : A⊢ C :: Δ ; Γ ⊢ᴺᵇ DB.shiftAbove 0 t : A grind [typing_shift (left := []) (right := Δ) (C := C)]All goals completed! 🐙

5.1.1.2. Substitution🔗

Removing one entry from the bound context corresponds to substituting a term of that entry's type. The three variable cases are the substituted variable itself, an earlier index, and a later index. Under a lambda, the argument is shifted and remains well-typed by weakening.

\frac{\Delta_1,\Delta_2;\Gamma \vdash s : C \qquad \Delta_1,C,\Delta_2;\Gamma \vdash e : A} {\Delta_1,\Delta_2;\Gamma \vdash [s/|\Delta_1|]e : A}

@[grind .] theorem typing_substitution
  (harg : left ++ right ; Γ ⊢ᴺᵇ arg : C)
  (hbody : left ++ C :: right ; Γ ⊢ᴺᵇ body : A)
  : left ++ right ; Γ ⊢ᴺᵇ DB.subst left.length arg body : A
:= byleft:BoundContextright:BoundContextΓ:FreeContextarg:DBC:Tybody:DBA:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : Chbody:left ++ C :: right ; Γ ⊢ᴺᵇ body : A⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg body : A induction body generalizing left right arg C A with
  | lam body ih =>lamΓ:FreeContextbody:DBih:∀ {left right : BoundContext} {arg : DB} {C A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg : C) →
    (left ++ C :: right ; Γ ⊢ᴺᵇ body : A) → left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg body : Aleft:BoundContextright:BoundContextarg:DBC:TyA:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : Chbody:left ++ C :: right ; Γ ⊢ᴺᵇ body.lam : A⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg body.lam : A
      cases hbody with
      | @lam D _ _ =>lam.lamΓ:FreeContextbody:DBih:∀ {left right : BoundContext} {arg : DB} {C A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg : C) →
    (left ++ C :: right ; Γ ⊢ᴺᵇ body : A) → left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg body : Aleft:BoundContextright:BoundContextarg:DBC:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : CD:TyB✝:Tya✝:D :: (left ++ C :: right) ; Γ ⊢ᴺᵇ body : B✝⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg body.lam : D ⇒ B✝
          grind [DB.subst, typing_shift_head (C := D) harg]All goals completed! 🐙
  | _ =>appΓ:FreeContextfn✝:DBarg✝:DBfn_ih✝:∀ {left right : BoundContext} {arg : DB} {C A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg : C) →
    (left ++ C :: right ; Γ ⊢ᴺᵇ fn✝ : A) → left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg fn✝ : Aarg_ih✝:∀ {left right : BoundContext} {arg : DB} {C A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg : C) →
    (left ++ C :: right ; Γ ⊢ᴺᵇ arg✝ : A) → left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg arg✝ : Aleft:BoundContextright:BoundContextarg:DBC:TyA:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : Chbody:left ++ C :: right ; Γ ⊢ᴺᵇ fn✝.app arg✝ : A⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg (fn✝.app arg✝) : AfreeΓ:FreeContextx✝:Stringleft:BoundContextright:BoundContextarg:DBC:TyA:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : Chbody:left ++ C :: right ; Γ ⊢ᴺᵇ DB.free x✝ : A⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg (DB.free x✝) : AboundΓ:FreeContextindex✝:ℕleft:BoundContextright:BoundContextarg:DBC:TyA:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : Chbody:left ++ C :: right ; Γ ⊢ᴺᵇ DB.bound index✝ : A⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg (DB.bound index✝) : A
      cases hbodyapp.appΓ:FreeContextfn✝:DBarg✝:DBfn_ih✝:∀ {left right : BoundContext} {arg : DB} {C A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg : C) →
    (left ++ C :: right ; Γ ⊢ᴺᵇ fn✝ : A) → left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg fn✝ : Aarg_ih✝:∀ {left right : BoundContext} {arg : DB} {C A : Ty},
  (left ++ right ; Γ ⊢ᴺᵇ arg : C) →
    (left ++ C :: right ; Γ ⊢ᴺᵇ arg✝ : A) → left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg arg✝ : Aleft:BoundContextright:BoundContextarg:DBC:TyA:Tyharg:left ++ right ; Γ ⊢ᴺᵇ arg : CA✝:Tya✝¹:left ++ C :: right ; Γ ⊢ᴺᵇ arg✝ : A✝a✝:left ++ C :: right ; Γ ⊢ᴺᵇ fn✝ : A✝ ⇒ A⊢ left ++ right ; Γ ⊢ᴺᵇ DB.subst (List.length left) arg (fn✝.app arg✝) : A
      all_goals grind [DB.subst, DB.HasType.app]All goals completed! 🐙

@[grind .] theorem typing_substitution_head
  (harg : Δ ; Γ ⊢ᴺᵇ arg : C)
  (hbody : C :: Δ ; Γ ⊢ᴺᵇ body : A)
  : Δ ; Γ ⊢ᴺᵇ DB.subst 0 arg body : A
:= byΔ:BoundContextΓ:FreeContextarg:DBC:Tybody:DBA:Tyharg:Δ ; Γ ⊢ᴺᵇ arg : Chbody:C :: Δ ; Γ ⊢ᴺᵇ body : A⊢ Δ ; Γ ⊢ᴺᵇ DB.subst 0 arg body : A grind [typing_substitution (left := []) (right := Δ)]All goals completed! 🐙

5.1.2. Preservation🔗

This is the first main result. Its beta case is exactly the substitution theorem; the remaining reduction rules follow from the induction hypotheses.

\frac{\Delta;\Gamma \vdash e : A \qquad e \to_\beta e'} {\Delta;\Gamma \vdash e' : A}

theorem preservation
  (hstep : t →βᵇ t')
  : (Δ ; Γ ⊢ᴺᵇ t : A) → (Δ ; Γ ⊢ᴺᵇ t' : A)
:= byt:DBt':DBΔ:BoundContextΓ:FreeContextA:Tyhstep:t →βᵇ t'⊢ (Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ t' : A intro htt:DBt':DBΔ:BoundContextΓ:FreeContextA:Tyhstep:t →βᵇ t'ht:Δ ; Γ ⊢ᴺᵇ t : A⊢ Δ ; Γ ⊢ᴺᵇ t' : A; induction hstep generalizing Δ Γ Abetat:DBt':DBbody✝:DBarg✝:DBΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ body✝.lam.app arg✝ : A⊢ Δ ; Γ ⊢ᴺᵇ DB.subst 0 arg✝ body✝ : Aapp_leftt:DBt':DBf✝:DBf'✝:DBa✝¹:DBa✝:f✝ →βᵇ f'✝a_ih✝:∀ {Δ : BoundContext} {Γ : FreeContext} {A : Ty}, (Δ ; Γ ⊢ᴺᵇ f✝ : A) → Δ ; Γ ⊢ᴺᵇ f'✝ : AΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ f✝.app a✝¹ : A⊢ Δ ; Γ ⊢ᴺᵇ f'✝.app a✝¹ : Aapp_rightt:DBt':DBa✝¹:DBa'✝:DBf✝:DBa✝:a✝¹ →βᵇ a'✝a_ih✝:∀ {Δ : BoundContext} {Γ : FreeContext} {A : Ty}, (Δ ; Γ ⊢ᴺᵇ a✝¹ : A) → Δ ; Γ ⊢ᴺᵇ a'✝ : AΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ f✝.app a✝¹ : A⊢ Δ ; Γ ⊢ᴺᵇ f✝.app a'✝ : Alamt:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ →βᵇ body'✝a_ih✝:∀ {Δ : BoundContext} {Γ : FreeContext} {A : Ty}, (Δ ; Γ ⊢ᴺᵇ body✝ : A) → Δ ; Γ ⊢ᴺᵇ body'✝ : AΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ body✝.lam : A⊢ Δ ; Γ ⊢ᴺᵇ body'✝.lam : A <;>betat:DBt':DBbody✝:DBarg✝:DBΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ body✝.lam.app arg✝ : A⊢ Δ ; Γ ⊢ᴺᵇ DB.subst 0 arg✝ body✝ : Aapp_leftt:DBt':DBf✝:DBf'✝:DBa✝¹:DBa✝:f✝ →βᵇ f'✝a_ih✝:∀ {Δ : BoundContext} {Γ : FreeContext} {A : Ty}, (Δ ; Γ ⊢ᴺᵇ f✝ : A) → Δ ; Γ ⊢ᴺᵇ f'✝ : AΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ f✝.app a✝¹ : A⊢ Δ ; Γ ⊢ᴺᵇ f'✝.app a✝¹ : Aapp_rightt:DBt':DBa✝¹:DBa'✝:DBf✝:DBa✝:a✝¹ →βᵇ a'✝a_ih✝:∀ {Δ : BoundContext} {Γ : FreeContext} {A : Ty}, (Δ ; Γ ⊢ᴺᵇ a✝¹ : A) → Δ ; Γ ⊢ᴺᵇ a'✝ : AΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ f✝.app a✝¹ : A⊢ Δ ; Γ ⊢ᴺᵇ f✝.app a'✝ : Alamt:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ →βᵇ body'✝a_ih✝:∀ {Δ : BoundContext} {Γ : FreeContext} {A : Ty}, (Δ ; Γ ⊢ᴺᵇ body✝ : A) → Δ ; Γ ⊢ᴺᵇ body'✝ : AΔ:BoundContextΓ:FreeContextA:Tyht:Δ ; Γ ⊢ᴺᵇ body✝.lam : A⊢ Δ ; Γ ⊢ᴺᵇ body'✝.lam : A grind [DB.HasType]All goals completed! 🐙

@[grind .] theorem preservation_star
  (hsteps : t →βᵇ* t')
  : (Δ ; Γ ⊢ᴺᵇ t : A) → (Δ ; Γ ⊢ᴺᵇ t' : A)
:= byt:DBt':DBΔ:BoundContextΓ:FreeContextA:Tyhsteps:t →βᵇ* t'⊢ (Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ t' : A induction hstepsreflt:DBt':DBΔ:BoundContextΓ:FreeContextA:Ty⊢ (Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ t : Atailt:DBt':DBΔ:BoundContextΓ:FreeContextA:Tyb✝:DBc✝:DBa✝¹:Relation.ReflTransGen DB.BetaStep t b✝a✝:b✝ →βᵇ c✝a_ih✝:(Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ b✝ : A⊢ (Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ c✝ : A <;>reflt:DBt':DBΔ:BoundContextΓ:FreeContextA:Ty⊢ (Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ t : Atailt:DBt':DBΔ:BoundContextΓ:FreeContextA:Tyb✝:DBc✝:DBa✝¹:Relation.ReflTransGen DB.BetaStep t b✝a✝:b✝ →βᵇ c✝a_ih✝:(Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ b✝ : A⊢ (Δ ; Γ ⊢ᴺᵇ t : A) → Δ ; Γ ⊢ᴺᵇ c✝ : A grind [preservation]All goals completed! 🐙

The same statement for any finite reduction sequence follows immediately by induction on the sequence.

5.1.3. Closed Normal Terms🔗

The key observation is that a typed neutral term must ultimately be headed by a variable from its context. If every type in that context is atomic, the head cannot be applied to an argument, so the whole neutral term is that variable. This is the neutrality lemma used in representation proofs.

theorem neutrality
  {atoms : List String}
  (hneutral : DB.Neutral t)
  (ht : atoms.map Ty.var ; [] ⊢ᴺᵇ t : B)
  : ∃ n X, t = .bound n ∧ atoms[n]? = some X ∧ B = .var X
:= byt:DBB:Tyatoms:List Stringhneutral:t.Neutralht:List.map Ty.var atoms ; [] ⊢ᴺᵇ t : B⊢ ∃ n X, t = DB.bound n ∧ atoms[n]? = some X ∧ B = Ty.var X
  cases hneutral with
  | app hfn _ =>appB:Tyatoms:List Stringfn✝:DBarg✝:DBhfn:fn✝.Neutrala✝:arg✝.Normalht:List.map Ty.var atoms ; [] ⊢ᴺᵇ fn✝.app arg✝ : B⊢ ∃ n X, fn✝.app arg✝ = DB.bound n ∧ atoms[n]? = some X ∧ B = Ty.var X
      cases htapp.appB:Tyatoms:List Stringfn✝:DBarg✝:DBhfn:fn✝.Neutrala✝²:arg✝.NormalA✝:Tya✝¹:List.map Ty.var atoms ; [] ⊢ᴺᵇ arg✝ : A✝a✝:List.map Ty.var atoms ; [] ⊢ᴺᵇ fn✝ : A✝ ⇒ B⊢ ∃ n X, fn✝.app arg✝ = DB.bound n ∧ atoms[n]? = some X ∧ B = Ty.var X
      grind [neutrality hfn]All goals completed! 🐙
  | _ =>freeB:Tyatoms:List Stringx✝:Stringht:List.map Ty.var atoms ; [] ⊢ᴺᵇ DB.free x✝ : B⊢ ∃ n X, DB.free x✝ = DB.bound n ∧ atoms[n]? = some X ∧ B = Ty.var XboundB:Tyatoms:List Stringn✝:ℕht:List.map Ty.var atoms ; [] ⊢ᴺᵇ DB.bound n✝ : B⊢ ∃ n X, DB.bound n✝ = DB.bound n ∧ atoms[n]? = some X ∧ B = Ty.var X
      cases htfree.freeB:Tyatoms:List Stringx✝:Stringa✝:List.lookup x✝ [] = some B⊢ ∃ n X, DB.free x✝ = DB.bound n ∧ atoms[n]? = some X ∧ B = Ty.var X
      grindAll goals completed! 🐙

In the empty context there is no variable that could head a neutral term. Consequently every closed, well-typed normal term is an abstraction.

Closed normal forms. If a closed, well-typed term is normal, then it is an abstraction.

@[grind .] theorem Neutral.not_typed_empty
  (hneutral : DB.Neutral t)
  : ¬ ([] ⊢ᵇ t : A)
:= byt:DBA:Tyhneutral:t.Neutral⊢ ¬[] ⊢ᵇ t : A grind [neutrality (atoms := []) hneutral]All goals completed! 🐙

theorem closed_normal_is_abstraction
  (ht : [] ⊢ᵇ t : A)
  (hnormal : DB.Normal t)
  : ∃ body, t = DB.lam body
:= byt:DBA:Tyht:[] ⊢ᵇ t : Ahnormal:t.Normal⊢ ∃ body, t = body.lam cases hnormallamA:Tybody✝:DBa✝:body✝.Normalht:[] ⊢ᵇ body✝.lam : A⊢ ∃ body, body✝.lam = body.lamneutralt:DBA:Tyht:[] ⊢ᵇ t : Aa✝:t.Neutral⊢ ∃ body, t = body.lam <;>lamA:Tybody✝:DBa✝:body✝.Normalht:[] ⊢ᵇ body✝.lam : A⊢ ∃ body, body✝.lam = body.lamneutralt:DBA:Tyht:[] ⊢ᵇ t : Aa✝:t.Neutral⊢ ∃ body, t = body.lam grindAll goals completed! 🐙

5.1.4. Representation of Booleans🔗

The Church Booleans share the type X → X → X: true returns its first argument and false returns its second. Conversely, these are the only closed normal terms of that type. Typing and normality first force two lambdas. The remaining body is a neutral term of type X in a context containing two variables of type X; neutrality says it must be one of those variables.

\cdot \vdash e : X \to X \to X \quad e\ \mathsf{normal} \quad\Longrightarrow\quad e = \lambda.\lambda.1 \;\text{or}\; e = \lambda.\lambda.0

theorem boolean_representation
  (ht : [] ⊢ᵇ t : Ty.var X ⇒ Ty.var X ⇒ Ty.var X)
  (hnormal : DB.Normal t)
  : t = DB[λ λ 1] ∨ t = DB[λ λ 0]
:= byt:DBX:Stringht:[] ⊢ᵇ t : Ty.var X ⇒ Ty.var X ⇒ Ty.var Xhnormal:t.Normal⊢ t = (DB.bound 1).lam.lam ∨ t = (DB.bound 0).lam.lam
  cases hnormal with
  | neutral hneutral =>neutralt:DBX:Stringht:[] ⊢ᵇ t : Ty.var X ⇒ Ty.var X ⇒ Ty.var Xhneutral:t.Neutral⊢ t = (DB.bound 1).lam.lam ∨ t = (DB.bound 0).lam.lam grindAll goals completed! 🐙
  | lam hbody =>lamX:Stringbody✝:DBhbody:body✝.Normalht:[] ⊢ᵇ body✝.lam : Ty.var X ⇒ Ty.var X ⇒ Ty.var X⊢ body✝.lam = (DB.bound 1).lam.lam ∨ body✝.lam = (DB.bound 0).lam.lam
      cases htlam.lamX:Stringbody✝:DBhbody:body✝.Normala✝:[Ty.var X] ; [] ⊢ᴺᵇ body✝ : Ty.var X ⇒ Ty.var X⊢ body✝.lam = (DB.bound 1).lam.lam ∨ body✝.lam = (DB.bound 0).lam.lam
      cases hbody with
      | neutral hneutral =>lam.lam.neutralX:Stringbody✝:DBa✝:[Ty.var X] ; [] ⊢ᴺᵇ body✝ : Ty.var X ⇒ Ty.var Xhneutral:body✝.Neutral⊢ body✝.lam = (DB.bound 1).lam.lam ∨ body✝.lam = (DB.bound 0).lam.lam grind [neutrality (atoms := [X]) hneutral]All goals completed! 🐙
      | lam hresult =>lam.lam.lamX:Stringbody✝:DBhresult:body✝.Normala✝:[Ty.var X] ; [] ⊢ᴺᵇ body✝.lam : Ty.var X ⇒ Ty.var X⊢ body✝.lam.lam = (DB.bound 1).lam.lam ∨ body✝.lam.lam = (DB.bound 0).lam.lam
          cases_type DB.HasTypelam.lam.lam.lamX:Stringbody✝:DBhresult:body✝.Normala✝:[Ty.var X, Ty.var X] ; [] ⊢ᴺᵇ body✝ : Ty.var X⊢ body✝.lam.lam = (DB.bound 1).lam.lam ∨ body✝.lam.lam = (DB.bound 0).lam.lam
          cases hresult with
          | lam =>lam.lam.lam.lam.lamX:Stringbody✝:DBa✝¹:body✝.Normala✝:[Ty.var X, Ty.var X] ; [] ⊢ᴺᵇ body✝.lam : Ty.var X⊢ body✝.lam.lam.lam = (DB.bound 1).lam.lam ∨ body✝.lam.lam.lam = (DB.bound 0).lam.lam grind [DB.HasType]All goals completed! 🐙
          | neutral hneutral =>lam.lam.lam.lam.neutralX:Stringbody✝:DBa✝:[Ty.var X, Ty.var X] ; [] ⊢ᴺᵇ body✝ : Ty.var Xhneutral:body✝.Neutral⊢ body✝.lam.lam = (DB.bound 1).lam.lam ∨ body✝.lam.lam = (DB.bound 0).lam.lam grind [neutrality (atoms := [X, X]) hneutral]All goals completed! 🐙

end DB

5.1.5. Named Presentation🔗

We now state the main results using the named terms that appear in mathematical writing. Their proofs use the de Bruijn development, but these named versions are the statements we will normally cite and apply later in the course.

namespace Term

5.1.5.1. Alpha-Equivalence🔗

Changing binder names does not affect typing, provided the corresponding binder types remain the same.

@[grind .] theorem typing_respects_alpha
  : (Δ.types = Δ'.types)
  → (e =α[Δ.names, Δ'.names] e')
  → (Δ ; Γ ⊢ᴺ e : A) → (Δ' ; Γ ⊢ᴺ e' : A)
:= bye:Terme':TermΔ:BinderContextΓ:FreeContextA:TyΔ':BinderContext⊢ Δ.types = Δ'.types → (e =α[Δ.names, Δ'.names] e') → (Δ ; Γ ⊢ᴺ e : A) → Δ' ; Γ ⊢ᴺ e' : A grind [Term.HasType]All goals completed! 🐙

5.1.5.2. Preservation🔗

Preservation. If a well-typed named term takes a beta step, its type is unchanged.

@[grind .] theorem preservation_with
  (hstep : e →β[Δ.names, Δ.names] e')
  : (Δ ; Γ ⊢ᴺ e : A) → (Δ ; Γ ⊢ᴺ e' : A)
:= bye:Terme':TermΔ:BinderContextΓ:FreeContextA:Tyhstep:e →β[Δ.names, Δ.names] e'⊢ (Δ ; Γ ⊢ᴺ e : A) → Δ ; Γ ⊢ᴺ e' : A grind [Term.HasType, DB.preservation]All goals completed! 🐙

@[grind .] theorem preservation_star_with
  (hsteps : e →β*[Δ.names, Δ.names] e')
  : (Δ ; Γ ⊢ᴺ e : A) → (Δ ; Γ ⊢ᴺ e' : A)
:= bye:Terme':TermΔ:BinderContextΓ:FreeContextA:Tyhsteps:e →β*[Δ.names, Δ.names] e'⊢ (Δ ; Γ ⊢ᴺ e : A) → Δ ; Γ ⊢ᴺ e' : A grind [Term.HasType]All goals completed! 🐙

theorem preservation
  (hstep : e →β e')
  : (Γ ⊢ e : A) → (Γ ⊢ e' : A)
:= bye:Terme':TermΓ:FreeContextA:Tyhstep:e →β e'⊢ (Γ ⊢ e : A) → Γ ⊢ e' : A grind [preservation_with (Δ := []) (Γ := Γ) hstep]All goals completed! 🐙

theorem preservation_star
  (hsteps : e →β* e')
  : (Γ ⊢ e : A) → (Γ ⊢ e' : A)
:= bye:Terme':TermΓ:FreeContextA:Tyhsteps:e →β* e'⊢ (Γ ⊢ e : A) → Γ ⊢ e' : A grind [preservation_star_with (Δ := []) (Γ := Γ) hsteps]All goals completed! 🐙

5.1.5.3. Closed Normal Terms🔗

Closed normal forms. A closed, well-typed named term that is normal must be a lambda abstraction.

theorem closed_normal_is_abstraction
  (ht : [] ⊢ e : A)
  (hnormal : Term.Normal e)
  : ∃ x body, e = .lam x body
:= bye:TermA:Tyht:[] ⊢ e : Ahnormal:e.Normal⊢ ∃ x body, e = Term.lam x body cases evarA:Tyx✝:Stringht:[] ⊢ Term.var x✝ : Ahnormal:(Term.var x✝).Normal⊢ ∃ x body, Term.var x✝ = Term.lam x bodylamA:Tyx✝:Stringbody✝:Termht:[] ⊢ Term.lam x✝ body✝ : Ahnormal:(Term.lam x✝ body✝).Normal⊢ ∃ x body, Term.lam x✝ body✝ = Term.lam x bodyappA:Tyfn✝:Termarg✝:Termht:[] ⊢ fn✝.app arg✝ : Ahnormal:(fn✝.app arg✝).Normal⊢ ∃ x body, fn✝.app arg✝ = Term.lam x body <;>varA:Tyx✝:Stringht:[] ⊢ Term.var x✝ : Ahnormal:(Term.var x✝).Normal⊢ ∃ x body, Term.var x✝ = Term.lam x bodylamA:Tyx✝:Stringbody✝:Termht:[] ⊢ Term.lam x✝ body✝ : Ahnormal:(Term.lam x✝ body✝).Normal⊢ ∃ x body, Term.lam x✝ body✝ = Term.lam x bodyappA:Tyfn✝:Termarg✝:Termht:[] ⊢ fn✝.app arg✝ : Ahnormal:(fn✝.app arg✝).Normal⊢ ∃ x body, fn✝.app arg✝ = Term.lam x body grind [DB.closed_normal_is_abstraction ht hnormal, Term.toDBWith]All goals completed! 🐙

5.1.5.4. Representation of Booleans🔗

Boolean representation. Up to alpha-equivalence, the only closed normal named terms of type X → X → X are the two Church Booleans λx. λy. x and λx. λy. y. This is the first representation theorem of the course: a type and normality together determine exactly which values it can represent.

theorem boolean_representation
  (ht : [] ⊢ e : Ty.var X ⇒ Ty.var X ⇒ Ty.var X)
  (hnormal : Term.Normal e)
  : e =α Term[λx. λy. x] ∨ e =α Term[λx. λy. y]
:= bye:TermX:Stringht:[] ⊢ e : Ty.var X ⇒ Ty.var X ⇒ Ty.var Xhnormal:e.Normal⊢ e =α Term.lam "x" (Term.lam "y" (Term.var "x")) ∨ e =α Term.lam "x" (Term.lam "y" (Term.var "y")) grind [Untyped.Term.AlphaEq, Untyped.Term.toDBWith, DB.boolean_representation ht hnormal]All goals completed! 🐙

end Termend SimplyTyped