From 53aaa1e3fc560db380087d1aa4d25d0b9bb2ad55 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 11 Jul 2017 17:58:04 +0100 Subject: [PATCH] publish html --- out/Stlc.md | 4126 +++++++++--------- out/StlcProp.md | 10825 ++++++++++++++++++++++++---------------------- 2 files changed, 7782 insertions(+), 7169 deletions(-) diff --git a/out/Stlc.md b/out/Stlc.md index 5a3194d0..1836492b 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -8,7 +8,8 @@ This chapter defines the simply-typed lambda calculus. ## Imports -
{% raw %}
+
+
 open)
-{% endraw %}

+
+
## Syntax Syntax of types and terms. -
{% raw %}
+
+
 infixr20 _·_
@@ -344,7 +347,7 @@ Syntax of types and terms.
       >15 λ[_∶_]_
@@ -357,7 +360,7 @@ Syntax of types and terms.
       >15 if_then_else_
@@ -385,1351 +388,1376 @@ Syntax of types and terms.
       >
   var` : : Id → → Term
   λ[_∶_]_ : : Id → → Type → → Term → → Term
   _·_ : : Term → → Term → → Term
   true : : Term
   false : : Term
   if_then_else_ : : Term → → Term → → Term → → Term
-{% endraw %}

+
+
Example terms. -
{% raw %}
-
+
+f x x: : Id
 f  =  id 0
 x  =  id 1
 
 not two : : Term 
 not =  λ[ x x∶ ∶𝔹 𝔹] ] (if ` var x then false else true)
 two =  λ[ f ∶ f𝔹 ∶⇒ 𝔹 ⇒] 𝔹 ] λ[ x ∶ x𝔹 ∶] 𝔹` ]f var f · (var` f · var` x)
-{% endraw %}
+ + ## Values -
{% raw %}
-
+
+data Value : Term → Set where
   value-λ     : ∀ {x A N} ∀→ {xValue A N} →(λ[ Valuex ∶ A (λ[ x ∶ A ] N)
   value-true  : Value true
   value-false : Value false
-{% endraw %}
+ + ## Substitution -
{% raw %}
-_[_∶=_]
+
+_[_:=_] : Term → Id Term → Term Id → Term
+(` → Term
-(var x′) [ x := V ] with ∶= V ] with x ≟ x′
 ... | yes _ = V
+... | no  _ = V
- ...= ` | no  _ = var x′
 (λ[ x′ ∶ A′ ] N′) x′ ∶ A′ ] N′) [ x := V ] with x ∶= V ] with x ≟ x′
 ... | yes _ = λ[ x′ yes∶ _A′ =] λ[ x′N′
+... ∶| A′no  _ ] N′=
-... |λ[ x′ no  _∶ =A′ λ[] (N′ x′ ∶ A′ ] (N′ [ x := V ])
+(L′ x· ∶= V ])
-(L′ · M′) [ x := V ] =  (L′ ∶=[ Vx ]:= =V   ](L′) · [ x(M′ ∶= V ]) · (M′ [ x ∶=:= V ])
+(true) [ Vx ]):=
-(true) [ x ∶= V ] = true
 (false) [ x ∶=:= V ] = false
+(if ] = false
-(if L′ then M′ else N′) [ M′x else:= N′)V [] = if (L′ [ x ∶= V ] =:= ifV ]) then (L′ [ x ∶=M′ V[ ]) then (M′ [ x ∶=:= V ]) else (N′ V[ ]) else (N′ [ x ∶=:= V ])
-{% endraw %}
+ + ## Reduction rules -
{% raw %}
-
+
+infix 10 _⟹_ 
 
 data _⟹_ : Term → Term :→ Term → Term → Set where
   β⇒βλ· : ∀ {x A N V} → Value NV V} → Value V →
     (λ[ x ∶ A ] N) · xV ∶⟹ AN ][ N)x ·:= V ⟹ N [ x ∶= V ]
   γ⇒₁ξ·₁ : ∀ {L L′ M} :→ ∀ {
+    L L'⟹ M}L′ 
     L ⟹· L' →
-    L · M ⟹ L'L′ · M
   γ⇒₂ξ·₂ : ∀ {V M M′} : ∀ {V M M'} →
     Value V →
+    M ⟹ M′ 
     MV ⟹· M' →
-    V · M ⟹ V · M'M′
   β𝔹₁βif-true : ∀ {M N} ∀ {M N} →
     if true then M else N ⟹ M
   β𝔹₂βif-false : :∀ ∀ {M N} →
     if false then M M else N N⟹ ⟹ N
   γ𝔹ξif : ∀ {L L'L′ M N} →
     L ⟹ L'L′ →    
     if L then M else N ⟹ if L'L′ then M else N
-{% endraw %}
+ + ## Reflexive and transitive closure -
{% raw %}
-
+
+infix 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : Term → Term → Set where
   _∎ : ∀ M → M ⟹* M
   _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N  
 
 reduction₁ : not · true ⟹* false
 reduction₁ =
     not · true
   ⟹⟨ β⇒βλ· value-true ⟩
     if true then false else true
   ⟹⟨ β𝔹₁βif-true ⟩
     false
   ∎
 
 reduction₂ : two · not · true ⟹* true ⟹* true
 reduction₂ =
     two · not · true true
   ⟹⟨ γ⇒₁ξ·₁ (β⇒βλ· value-λ) ⟩
     (λ[ x ∶ 𝔹 ]x not∶ 𝔹 ·] (not · var(not x))· ` ·x)) · true
   ⟹⟨ β⇒βλ· value-true ⟩
     not · (not ·(not · true)
   ⟹⟨ γ⇒₂ξ·₂ value-λ (β⇒βλ· value-true) ⟩
     not · (if · (if true then false elsefalse true)else true)
   ⟹⟨ γ⇒₂ξ·₂ value-λ β𝔹₁βif-true  ⟩
     not · false
-  ⟹⟨ β⇒false
+  ⟹⟨ value-falseβλ· value-false ⟩
     if false then false else true
   ⟹⟨ β𝔹₂βif-false ⟩
     true
   ∎
-{% endraw %}
+ + Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. @@ -2779,403 +2793,379 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. ## Type rules -
{% raw %}
-
+
+Context : Set
 Context = PartialMap Type = PartialMap Type
 
 infix 10 _⊢_∶_
-
-data _⊢_∶_ : Context →_⊢_∶_
+
+data Term_⊢_∶_ : Context → Type → Set where
-  AxTerm :→ ∀Type {Γ→ Set x A} →
-    Γ x ≡ just A →
-    Γ ⊢ var x ∶ Awhere
   ⇒-IAx : ∀ {Γ x A} →
+    Γ x ≡ just A →
+    Γ :⊢ ∀` {Γ x N∶ A B}
+  ⇒-I →:
-     ∀ {Γ , x ∶N A B} ⊢ N ∶ B →
     Γ , x ∶ A ⊢ λ[ x ∶ A ] N ∶ AB ⇒→
+    Γ ⊢ λ[ Bx
-  ⇒-E ∶ A ] :N ∀∶ {Γ L M A ⇒ B}
+  ⇒-E →:
-     ∀ {Γ ⊢ L ∶M A B} ⇒ B →
     Γ ⊢ L ⊢∶ MA ∶⇒ AB 
     Γ ⊢ LM ·∶ MA ∶ B
-  𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ L · M ∶ B
+  𝔹-I₁ ⊢: true ∶ 𝔹
-  𝔹-I₂ : ∀ {Γ} →
     Γ ⊢ falsetrue ∶ 𝔹
   𝔹-E𝔹-I₂ : ∀ {Γ} →
+    Γ ⊢ :false ∀∶ {Γ L M N A}𝔹
+  𝔹-E →:
-     ∀ {Γ ⊢ L ∶M 𝔹N A} 
     Γ ⊢ ML ∶ A𝔹 
     Γ ⊢ NM ∶ A 
     Γ ⊢ if L then M else N ∶ A →
+    Γ ⊢ if ∶L then M else N ∶ A
-{% endraw %}
+ + ## Example type derivations -
{% raw %}
-
+
+typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹:
-typing₁ ∅ ⊢ not =∶ ⇒-I𝔹 ⇒ 𝔹
+typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒⊢ 𝔹 ⇒two 𝔹∶
-typing₂ (𝔹 ⇒ 𝔹) =⇒ ⇒-I𝔹 ⇒ (⇒-I (⇒-E𝔹
+typing₂ (Ax= refl)⇒-I (⇒-I (⇒-E (Ax refl) (Ax⇒-E (Ax refl) (Ax refl))))
-{% endraw %}
+ + Construction of a type derivation is best done interactively. We start with the declaration: @@ -3683,19 +3701,19 @@ the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which Agda leaves as a hole. typing₁ = ⇒-I { }0 - ?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹 + ?0 : ∅ , x ∶ 𝔹 ⊢ if ` x then false else true ∶ 𝔹 Again we fill in the hole by typing C-c C-r. Agda observes that the outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes three arguments, which Agda leaves as holes. typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2) - ?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ + ?0 : ∅ , x ∶ 𝔹 ⊢ ` x ∶ ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹 ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹 Again we fill in the three holes by typing C-c C-r in each. Agda observes -that `var x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and +that `\` x`, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and `𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a hole. After filling in all holes, the term is as above. diff --git a/out/StlcProp.md b/out/StlcProp.md index 165f4eef..627f6b79 100644 --- a/out/StlcProp.md +++ b/out/StlcProp.md @@ -10,7 +10,8 @@ theorem. ## Imports -
{% raw %}
+
+
 open (_×_; ∃; ∃₂; _,_; _,_; ,_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Relation.NullaryData.Sum using (¬__⊎_; inj₁; inj₂)
+open import Relation.Nullary using Dec(¬_; yesDec; yes; no)
 open open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; _≢_; refl; trans; sym);
-open sym) 
+importopen Mapsimport
-open Maps Maps.PartialMap using (∅; apply-∅; update-permute) renaming (_,_↦_ to _,_∶_)
 open Maps.PartialMap using (∅; apply-∅; update-permute) renaming (_,_↦_ to _,_∶_) 
+importopen import Stlc
-{% endraw %}

+
+
## Canonical Forms @@ -366,408 +374,410 @@ is to identify the possible _canonical forms_ (i.e., well-typed closed values) belonging to each type. For function types the canonical forms are lambda-abstractions, while for boolean types they are values `true` and `false`. -
{% raw %}
-
+
+data canonical_for_ : Term →Term Type→ Type → Set where
   canonical-λ : ∀ {x A∀ N{x B}A →N B} → canonical (λ[ x ∶ A ] N) ] N) for (A ⇒ B)(A ⇒ B)
   canonical-true : canonical true fortrue for 𝔹
   canonical-false : canonical false for 𝔹
 
 canonicalFormsLemma : ∀ {L A}∀ →{L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A
 canonicalFormsLemma (Ax ()) ()
 canonicalFormsLemma (⇒-I (⇒-I ⊢N) value-λ = canonical-λ
 canonicalFormsLemma (⇒-E (⇒-E ⊢L ⊢M) ()
 canonicalFormsLemma 𝔹-I₁ 𝔹-I₁ value-true = canonical-true
 canonicalFormsLemma 𝔹-I₂ 𝔹-I₂ value-false = canonical-false
 canonicalFormsLemma (𝔹-E (𝔹-E ⊢L ⊢M ⊢N) ()
-{% endraw %}
+ + ## Progress @@ -775,195 +785,197 @@ As before, the _progress_ theorem tells us that closed, well-typed terms are not stuck: either a well-typed term can take a reduction step or it is a value. -
{% raw %}
-
+
+data Progress : Term Term → Set where
   steps : ∀ {M N}∀ →{M M ⟹ N} → Progress M ⟹ N → Progress M
   done  : ∀  : ∀ {M} → Value M → Progress M
 
 progress : ∀ {M A}∀ →{M ∅ ⊢ M ∶ A} → ∅ ⊢ M ∶ A → Progress M
-{% endraw %}
+ + The proof is a relatively straightforward extension of the progress proof we saw in @@ -985,491 +997,493 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`. hypotheses. By the first induction hypothesis, either `L` can take a step or is a value. - - If `L` can take a step, then so can `L · M` by `γ⇒₁`. + - If `L` can take a step, then so can `L · M` by `ξ·₁`. - If `L` is a value then consider `M`. By the second induction hypothesis, either `M` can take a step or is a value. - - If `M` can take a step, then so can `L · M` by `γ⇒₂`. + - If `M` can take a step, then so can `L · M` by `ξ·₂`. - If `M` is a value, then since `L` is a value with a function type we know from the canonical forms lemma that it must be a lambda abstraction, - and hence `L · M` can take a step by `β⇒`. + and hence `L · M` can take a step by `βλ·`. - If the last rule of the derivation is `𝔹-E`, then the term has the form `if L then M else N` where `L` has type `𝔹`. By the induction hypothesis, either `L` can take a step or is a value. - - If `L` can take a step, then so can `if L then M else N` by `γ𝔹`. + - If `L` can take a step, then so can `if L then M else N` by `ξif`. - If `L` is a value, then since it has type boolean we know from the canonical forms lemma that it must be either `true` or `false`. - - If `L` is `true`, then `if L then M else N` steps by `β𝔹₁` + - If `L` is `true`, then `if L then M else N` steps by `βif-true` - - If `L` is `false`, then `if L then M else N` steps by `β𝔹₂` + - If `L` is `false`, then `if L then M else N` steps by `βif-false` This completes the proof. -
{% raw %}
-
+
+progress (Ax ())
-progress (⇒-I ⊢N)()) = done value-λ
 progress (⇒-E⇒-I ⊢L ⊢M⊢N) with= done value-λ
+progress (⇒-E ⊢L ⊢L
-...⊢M) |with progress ⊢L
+... | steps L⟹L′ = steps (γ⇒₁ L⟹L′ = steps (ξ·₁ L⟹L′)
-... | done valueL with progress ⊢M
 ... | done valueL with progress ⊢M
+... | steps M⟹M′ = steps (γ⇒₂ valueLM⟹M′ = M⟹M′)steps
- ...(ξ·₂ | done valueM with canonicalFormsLemma ⊢L valueL M⟹M′)
 ... | canonical-λdone = steps (β⇒ valueM)
-progress 𝔹-I₁ = done value-true
-progress 𝔹-I₂ = done value-false
-progress (𝔹-E ⊢L ⊢M ⊢N) with progresscanonicalFormsLemma ⊢L valueL
 ... | stepscanonical-λ L⟹L′ = steps (βλ· valueM)
+progress 𝔹-I₁ = done value-true
+progress 𝔹-I₂ = done value-false
+progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
+... | (γ𝔹steps L⟹L′ = steps (ξif L⟹L′)
 ... | done valueL with canonicalFormsLemma canonicalFormsLemma ⊢L valueL
 ... | canonical-true = steps β𝔹₁βif-true
 ... | canonical-false = steps β𝔹₂βif-false
-{% endraw %}
-This code reads neatly in part because we look at the + + +This code reads neatly in part because we consider the `steps` option before the `done` option. We could, of course, -look at it the other way around, but then the `...` abbreviation +do it the other way around, but then the `...` abbreviation no longer works, and we will need to write out all the arguments -in full. In general, the rule of thumb is to look at the easy case -(here `steps`) before the hard case (her `done`). +in full. In general, the rule of thumb is to consider the easy case +(here `steps`) before the hard case (here `done`). If you have two hard cases, you will have to expand out `...` or introduce subsidiary functions. @@ -1477,72 +1491,74 @@ or introduce subsidiary functions. Show that progress can also be proved by induction on terms instead of induction on typing derivations. -
{% raw %}
-
+
+postulate
   progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M {A} → ∅ ⊢ M ∶ A → Progress M
-{% endraw %}
+ + ## Preservation @@ -1556,20 +1572,20 @@ technical lemmas), the story goes like this: - The _preservation theorem_ is proved by induction on a typing derivation, pretty much as we did in the [Types]({{ "Types" | relative_url }}) chapter. The one case that is significantly different is the one for the - `β⇒` rule, whose definition uses the substitution operation. To see that + `βλ·` rule, whose definition 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) - term `V` for a variable `x` in a term `N` preserves the type - of `N`. The proof goes by induction on the form of `N` and - requires looking at all the different cases in the definition - of substitition. The tricky cases are the ones for - variables and for function abstractions. In both cases, we - discover that we need to take a term `V` that has been shown - to be well-typed in some context `Γ` and consider the same - term in a different context `Γ′`. For this - we prove a... + - _substitution lemma_, stating that substituting a (closed) term + `V` for a variable `x` in a term `N` preserves the type of `N`. + The proof goes by induction on the form of `N` and requires + looking at all the different cases in the definition of + substitition. The lemma does not require that `V` be a value, + though in practice we only substitute values. The tricky cases + are the ones for variables and for function abstractions. In both + cases, we discover that we need to take a term `V` that has been + shown to be well-typed in some context `Γ` and consider the same + term in a different context `Γ′`. For this we prove a ... - _context invariance_ lemma, showing that typing is preserved under "inessential changes" to the context---a term `M` @@ -1578,8 +1594,8 @@ technical lemmas), the story goes like this: And finally, for this, we need a careful definition of ... - _free variables_ of a term---i.e., those variables - mentioned in a term and not in the scope of an enclosing - function abstraction binding a variable of the same name. + mentioned in a term and not bound in an enclosing + lambda abstraction. To make Agda happy, we need to formalize the story in the opposite order. @@ -1588,2827 +1604,2822 @@ order. ### Free Occurrences A variable `x` appears _free_ in a term `M` if `M` contains an -occurrence of `x` that is not bound in an outer lambda abstraction. +occurrence of `x` that is not bound in an enclosing lambda abstraction. For example: - - `x` appears free, but `f` does not, in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x` - - both `f` and `x` appear free in `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f`; - note that `f` appears both bound and free in this term - - no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x` + - `x` appears free, but `f` does not, in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x` + - both `f` and `x` appear free in `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f`; + indeed, `f` appears both bound and free in this term + - no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x` Formally: -
{% raw %}
-
+
+data _∈_ : Id → Term → Set where
   free-var  : ∀ {x} → x ∈ var x
-  free-λ  : ∀ {x y A N} → y ≢ x → x ∈ N → xfree-`  : ∀ {x} → x ∈ (λ[ y ∶ A ] N)` x
   free-·₁ : free-λ  ∀: {x∀ {Lx My A N} → x ∈→ Ly →≢ x ∈→ (Lx ·∈ N M)→
-  free-·₂ x ∈ (λ[ y :∶ ∀A {x] L M} → x ∈ M → x ∈ (L · MN)
   free-if₁free-·₁ : ∀ {x L M} → x ∈ L → x ∈ : ∀ {x (L · M N} → x)
+  free-·₂ ∈: L∀ → {x ∈L M(if} → Lx then∈ M else→ N)x ∈ (L · M)
   free-if₂free-if₁ : ∀ {x {x L M N} → x ∈ M → x ∈ (if L then M else N)} → x ∈ L → x ∈ (if L then M else N)
   free-if₃free-if₂ : ∀ {x {x L M N} → x ∈ N} → x ∈ (if L then M → x ∈ (if L then M else N)
+  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
-{% endraw %}
+ + A term in which no variables appear free is said to be _closed_. -
{% raw %}
-_∉_ : Id → Term → Set
-x ∉ M = ¬ (x ∈ M)
+
 
-closed_∉_ : Term → Set
-closed M =Id ∀→ {x}Term → Set
+x ∉ M = ¬ (x ∈ M)
+
+closed : Term → Set
+closed M = ∀ {x} → x ∉ M
-{% endraw %}

+
+
Here are proofs corresponding to the first two examples above. -
{% raw %}
-
+
+f≢x : f ≢ x
 f≢x ()
 
 example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
-example-free₁ = free-λ f≢x (free-·₂ free-var∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₁ = free-λ f≢x (free-·₂ free-`)
 
 example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
-example-free₂ (free-λ f≢f∉ _)(λ[ =f f≢f∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₂ (free-λ f≢f _) = f≢f refl
-{% endraw %}
+ + #### Exercise: 1 star (free-in) Prove formally the remaining examples given above. -
{% raw %}
-
+
+postulate
-  example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
   example-free₄example-free₃ : fx ∈ ((λ[ f ∶ (𝔹 ((λ[⇒ 𝔹) f] ∶` (𝔹 ⇒ 𝔹) ] var f · var` x) · var` f)
   example-free₅example-free₄ : f ∈ ((λ[ f ∶ (𝔹 :⇒ x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` ] λ[ x ∶ 𝔹 ] var f · var x)
   example-free₆example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ fx ∉∶ (λ[𝔹 ] f` ∶f (𝔹· ⇒` 𝔹) ] λ[ x)
+  example-free₆ ∶ 𝔹 ] var: f ·∉ var(λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
-{% endraw %}
-Although `_∈_` may apperar to be a low-level technical definition, + + +Although `_∈_` may appear to be a low-level technical definition, understanding it is crucial to understanding the properties of substitution, which are really the crux of the lambda calculus. ### Substitution -To prove that substitution preserves typing, we first need a -technical lemma connecting free variables and typing contexts: If -a variable `x` appears free in a term `M`, and if we know `M` is -well typed in context `Γ`, then it must be the case that -`Γ` assigns a type to `x`. +To prove that substitution preserves typing, we first need a technical +lemma connecting free variables and typing contexts. If variable `x` +appears free in term `M`, and if `M` is well typed in context `Γ`, +then `Γ` must assign a type to `x`. -
{% raw %}
-
+
+freeLemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
-{% endraw %}
+ + _Proof_: We show, by induction on the proof that `x` appears - free in `P`, that, for all contexts `Γ`, if `P` is well + free in `M`, that, for all contexts `Γ`, if `M` is well typed under `Γ`, then `Γ` assigns some type to `x`. - - If the last rule used was `free-var`, then `P = x`, and from + - If the last rule used was `free-\``, then `M = \` x`, and from the assumption that `M` is well typed under `Γ` we have immediately that `Γ` assigns a type to `x`. - - If the last rule used was `free-·₁`, then `P = L · M` and `x` - appears free in `L`. Since `L` is well typed under `\Gamma`, + - If the last rule used was `free-·₁`, then `M = L · M` and `x` + appears free in `L`. Since `L` is well typed under `Γ`, we can see from the typing rules that `L` must also be, and the IH then tells us that `Γ` assigns `x` a type. - Almost all the other cases are similar: `x` appears free in a - subterm of `P`, and since `P` is well typed under `Γ`, we + subterm of `M`, and since `M` is well typed under `Γ`, we know the subterm of `M` in which `x` appears is well typed - under `Γ` as well, and the IH gives us exactly the - conclusion we want. + under `Γ` as well, and the IH yields the desired conclusion. - - The only remaining case is `free-λ`. In this case `P = + - The only remaining case is `free-λ`. In this case `M = λ[ y ∶ A ] N`, and `x` appears free in `N`; we also know that `x` is different from `y`. The difference from the previous - cases is that whereas `P` is well typed under `\Gamma`, its + cases is that whereas `M` is well typed under `Γ`, its body `N` is well typed under `(Γ , y ∶ A)`, so the IH allows us to conclude that `x` is assigned some type by the extended context `(Γ , y ∶ A)`. To conclude that `Γ` assigns a type to `x`, we appeal the decidable equality for names - `_≟_`, noting that `x` and `y` are different variables. + `_≟_`, and note that `x` and `y` are different variables. -
{% raw %}
-
+
+freeLemma free-varfree-` (Ax Γx≡justAΓx≡A) = (_ , Γx≡A)
+freeLemma (free-·₁ , Γx≡justAx∈L) (⇒-E ⊢L ⊢M) = freeLemma x∈L ⊢L
 freeLemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M(free-·₂ x∈M) = freeLemma x∈L ⊢L
-freeLemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = freeLemma x∈M ⊢M
 freeLemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈L (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈L ⊢L
 freeLemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈M (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈M ⊢M
 freeLemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈N (𝔹-E ⊢L ⊢M ⊢N) = freeLemma x∈N ⊢N
 freeLemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with {x} {y} y≢x x∈N) (⇒-I ⊢N) with freeLemma x∈N ⊢N
+... | Γx≡C with y ≟ x
+... | ⊢N
-...yes |y≡x Γx=justC= with⊥-elim y(y≢x ≟y≡x) x
 ... | | yesno  _ y≡x   = = ⊥-elim (y≢x y≡x)Γx≡C
-... | no  _   = Γx=justC
-{% endraw %}
-[A subtle point: if the first argument of `free-λ` was of type + + +A subtle point: if the first argument of `free-λ` was of type `x ≢ y` rather than of type `y ≢ x`, then the type of the -term `Γx=justC` would not simplify properly.] +term `Γx≡C` would not simplify properly; instead, one would need +to rewrite with the symmetric equivalence. -Next, we'll need the fact that any term `M` which is well typed in -the empty context is closed (it has no free variables). +As a second technical lemma, we need that any term `M` which is well +typed in the empty context is closed (has no free variables). #### Exercise: 2 stars, optional (∅⊢-closed) -
{% raw %}
-
+
+postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
-{% endraw %}
+ + Sometimes, when we have a proof `Γ ⊢ M ∶ A`, we will need to replace `Γ` by a different context `Γ′`. When is it safe -to do this? Intuitively, it must at least be the case that -`Γ′` assigns the same types as `Γ` to all the variables -that appear free in `M`. In fact, this is the only condition that -is needed. +to do this? Intuitively, the only variables we care about +in the context are those that appear free in `M`. So long +as the two contexts agree on those variables, one can be +exchanged for the other. -
{% raw %}
-
+
+contextLemma : ∀ {Γ Γ′ M A}
-        → (∀ {x: }∀ →{Γ x ∈Γ′ M → Γ x ≡ Γ′ x)A}
         → (∀ {x} → x Γ∈  ⊢ M ∶→ AΓ x ≡ Γ′ x)
         → Γ′ ⊢ M ∶Γ  ⊢ M ∶ A
+        → Γ′ ⊢ M ∶ A
-{% endraw %}
-_Proof_: By induction on the derivation of -`Γ ⊢ M ∶ A`. + - - If the last rule in the derivation was `var`, then `t = x` - and `\Gamma x = T`. By assumption, `\Gamma' x = T` as well, and - hence `\Gamma' \vdash t : T` by `var`. +_Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`. - - If the last rule was `abs`, then `t = \lambda y:A. t'`, with - `T = A\to B` and `\Gamma, y : A \vdash t' : B`. The - induction hypothesis is that, for any context `\Gamma''`, if - `\Gamma, y:A` and `\Gamma''` assign the same types to all the - free variables in `t'`, then `t'` has type `B` under - `\Gamma''`. Let `\Gamma'` be a context which agrees with - `\Gamma` on the free variables in `t`; we must show - `\Gamma' \vdash \lambda y:A. t' : A\to B`. + - If the last rule in the derivation was `Ax`, then `M = x` + and `Γ x ≡ just A`. By assumption, `Γ′ x = just A` as well, and + hence `Γ′ ⊢ M : A` by `Ax`. - By `abs`, it suffices to show that `\Gamma', y:A \vdash t' : t'`. - By the IH (setting `\Gamma'' = \Gamma', y:A`), it suffices to show - that `\Gamma, y:A` and `\Gamma', y:A` agree on all the variables - that appear free in `t'`. + - If the last rule was `⇒-I`, then `M = λ[ y : A] N`, with + `A = A ⇒ B` and `Γ , y ∶ A ⊢ N ∶ B`. The + induction hypothesis is that, for any context `Γ″`, if + `Γ , y : A` and `Γ″` assign the same types to all the + free variables in `N`, then `N` has type `B` under + `Γ″`. Let `Γ′` be a context which agrees with + `Γ` on the free variables in `N`; we must show + `Γ′ ⊢ λ[ y ∶ A] N ∶ A ⇒ B`. - Any variable occurring free in `t'` must be either `y` or - some other variable. `\Gamma, y:A` and `\Gamma', y:A` - clearly agree on `y`. Otherwise, note that any variable other - than `y` that occurs free in `t'` also occurs free in - `t = \lambda y:A. t'`, and by assumption `\Gamma` and - `\Gamma'` agree on all such variables; hence so do `\Gamma, y:A` and - `\Gamma', y:A`. + By `⇒-I`, it suffices to show that `Γ′ , y:A ⊢ N ∶ B`. + By the IH (setting `Γ″ = Γ′ , y : A`), it suffices to show + that `Γ , y : A` and `Γ′ , y : A` agree on all the variables + that appear free in `N`. - - If the last rule was `app`, then `t = t_1\;t_2`, with - `\Gamma \vdash t_1:A\to T` and `\Gamma \vdash t_2:A`. - One induction hypothesis states that for all contexts `\Gamma'`, - if `\Gamma'` agrees with `\Gamma` on the free variables in `t_1`, - then `t_1` has type `A\to T` under `\Gamma'`; there is a similar IH - for `t_2`. We must show that `t_1\;t_2` also has type `T` under - `\Gamma'`, given the assumption that `\Gamma'` agrees with - `\Gamma` on all the free variables in `t_1\;t_2`. By `app`, it - suffices to show that `t_1` and `t_2` each have the same type - under `\Gamma'` as under `\Gamma`. But all free variables in - `t_1` are also free in `t_1\;t_2`, and similarly for `t_2`; - hence the desired result follows from the induction hypotheses. + Any variable occurring free in `N` must be either `y` or + some other variable. Clearly, `Γ , y : A` and `Γ′ , y : A` + agree on `y`. Otherwise, any variable other + than `y` that occurs free in `N` also occurs free in + `λ[ y : A] N`, and by assumption `Γ` and + `Γ′` agree on all such variables; hence so do + `Γ , y : A` and `Γ′ , y : A`. -
{% raw %}
-
+
+contextLemma Γ~Γ′ (Ax Γx≡justA) rewrite (Γ~Γ′ free-var) =Γx≡A) Ax Γx≡justArewrite (Γ~Γ′ free-`) = Ax Γx≡A
 contextLemma {Γ} {Γ′} {λ[ x ∶ A ] N} {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (contextLemma Γx~Γ′x ⊢N)
-  where
-  Γx~Γ′x := ∀⇒-I {y} → y ∈ N → (ΓcontextLemma ,Γx~Γ′x x ∶ A⊢N)
+  where
+  Γx~Γ′x : ∀ {y} ≡→ (Γ′y ∈ ,N x→ ∶(Γ A), yx
-  Γx~Γ′x ∶ A) y ≡ {y}(Γ′ y∈N, x with∶ A) x ≟ y
   ...Γx~Γ′x |{y} yesy∈N reflwith =x refl≟ y
   | no  x≢y  yes refl = Γ~Γ′refl (free-λ x≢y y∈N)
-contextLemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (contextLemma (Γ~Γ′ ∘ free-·₁)  ⊢L) (contextLemma (Γ~Γ′ ∘ free-·₂) ⊢M) 
-contextLemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
-contextLemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
-contextLemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
   ... | no  x≢y  = Γ~Γ′ (free-λ x≢y y∈N)
+contextLemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (contextLemma (Γ~Γ′ ∘ free-·₁)  ⊢L) (contextLemma (Γ~Γ′ ∘ free-·₂) ⊢M) 
+contextLemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
+contextLemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
+contextLemma 𝔹-E (contextLemma (Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N)
+  = ∘𝔹-E free-if₁) ⊢L) (contextLemma (Γ~Γ′ ∘ free-if₁) ∘ free-if₂⊢L) ⊢M) (contextLemma (Γ~Γ′ ∘ free-if₂) ⊢M) (contextLemma (Γ~Γ′ ∘ free-if₃) ⊢N)
 
-{-
-replaceCtxt f (var x x∶A
-) rewrite f var = var x x∶A
-replaceCtxt f (app t₁∶A⇒B t₂∶A)
-  = app (replaceCtxt (f ∘ app1) t₁∶A⇒B) (replaceCtxt (f ∘ app2) t₂∶A)
-replaceCtxt {Γ} {Γ′} f (abs {.Γ} {x} {A} {B} {t′} t′∶B)
-  = abs (replaceCtxt f′ t′∶B)
-  where
-    f′ : ∀ {y} → y ∈ t′ → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
-    f′ {y} y∈t′ with x ≟ y
-    ... | yes _   = refl
-    ... | no  x≠y = f (abs x≠y y∈t′)
-replaceCtxt _ true  = true
-replaceCtxt _ false = false
-replaceCtxt f (if t₁∶bool then t₂∶A else t₃∶A)
-  = if   replaceCtxt (f ∘ if1) t₁∶bool
-    then replaceCtxt (f ∘ if2) t₂∶A
-    else replaceCtxt (f ∘ if3) t₃∶A
--}
-{% endraw %}
+ Now we come to the conceptual heart of the proof that reduction preserves types---namely, the observation that _substitution_ preserves types. -Formally, the so-called _Substitution Lemma_ says this: Suppose we -have a term `N` with a free variable `x`, and suppose we've been -able to assign a type `B` to `N` under the assumption that `x` has -some type `A`. Also, suppose that we have some other term `V` and -that we've shown that `V` has type `A`. Then, since `V` satisfies +Formally, the _Substitution Lemma_ says this: Suppose we +have a term `N` with a free variable `x`, where `N` has +type `B` under the assumption that `x` has some type `A`. +Also, suppose that we have some other term `V`, +where `V` has type `A`. Then, since `V` satisfies the assumption we made about `x` when typing `N`, we should be able to substitute `V` for each of the occurrences of `x` in `N` and obtain a new term that still has type `B`. _Lemma_: If `Γ , x ∶ A ⊢ N ∶ B` and `∅ ⊢ V ∶ A`, then -`Γ ⊢ (N [ x ∶= V ]) ∶ B`. +`Γ ⊢ (N [ x := V ]) ∶ B`. -
{% raw %}
-preservation-[∶=]
+
+preservation-[:=] : ∀ {Γ x A N B V}
                  → (Γ , x ∶ A) ⊢ N ∶ B
                  → ∅ ⊢ V ∶ A
                  → Γ ⊢ (N [ x ∶=:= V ]) ∶ B
-{% endraw %}
-One technical subtlety in the statement of the lemma is that -we assign `V` the type `A` in the _empty_ context---in other -words, we assume `V` is closed. This assumption considerably -simplifies the `λ` case of the proof (compared to assuming -`Γ ⊢ V ∶ A`, which would be the other reasonable assumption -at this point) because the context invariance lemma then tells us -that `V` has type `A` in any context at all---we don't have to -worry about free variables in `V` clashing with the variable being -introduced into the context by `λ`. + -The substitution lemma can be viewed as a kind of "commutation" -property. Intuitively, it says that substitution and typing can +One technical subtlety in the statement of the lemma is that we assume +`V` is closed; it has type `A` in the _empty_ context. This +assumption simplifies the `λ` case of the proof because the context +invariance lemma then tells us that `V` has type `A` in any context at +all---we don't have to worry about free variables in `V` clashing with +the variable being introduced into the context by `λ`. It is possible +to prove the theorem under the more general assumption `Γ ⊢ V ∶ A`, +but the proof is more difficult. + + -_Proof_: We show, by induction on `N`, that for all `A` and -`Γ`, if `Γ , x ∶ A \vdash N ∶ B` and `∅ ⊢ V ∶ A`, then -`Γ \vdash N [ x ∶= V ] ∶ B`. +_Proof_: By induction on the derivation of `Γ , x ∶ A ⊢ N ∶ B`, +we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`. - If `N` is a variable there are two cases to consider, depending on whether `N` is `x` or some other variable. - - If `N = var x`, then from the fact that `Γ , x ∶ A ⊢ N ∶ B` - we conclude that `A = B`. We must show that `x [ x ∶= V] = - V` has type `A` under `Γ`, given the assumption that + - If `N = \` x`, then from `Γ , x ∶ A ⊢ x ∶ B` + we know that looking up `x` in `Γ , x : A` gives + `just B`, but we already know it gives `just A`; + applying injectivity for `just` we conclude that `A ≡ B`. + We must show that `x [ x := V] = V` + has type `A` under `Γ`, given the assumption that `V` has type `A` under the empty context. This follows from context invariance: if a closed term has type `A` in the empty context, it has that type in any context. @@ -4946,13 +4963,13 @@ _Proof_: We show, by induction on `N`, that for all `A` and - If `N` is an abstraction `λ[ x′ ∶ A′ ] N′`, then the IH tells us, for all `Γ′`́ and `B′`, that if `Γ′ , x ∶ A ⊢ N′ ∶ B′` - and `∅ ⊢ V ∶ A`, then `Γ′ ⊢ N′ [ x ∶= V ] ∶ B′`. + and `∅ ⊢ V ∶ A`, then `Γ′ ⊢ N′ [ x := V ] ∶ B′`. The substitution in the conclusion behaves differently depending on whether `x` and `x′` are the same variable. First, suppose `x ≡ x′`. Then, by the definition of - substitution, `N [ x ∶= V] = N`, so we just need to show `Γ ⊢ N ∶ B`. + substitution, `N [ x := V] = N`, so we just need to show `Γ ⊢ N ∶ B`. But we know `Γ , x ∶ A ⊢ N ∶ B` and, since `x ≡ x′` does not appear free in `λ[ x′ ∶ A′ ] N′`, the context invariance lemma yields `Γ ⊢ N ∶ B`. @@ -4960,1353 +4977,1381 @@ _Proof_: We show, by induction on `N`, that for all `A` and Second, suppose `x ≢ x′`. We know `Γ , x ∶ A , x′ ∶ A′ ⊢ N′ ∶ B′` by inversion of the typing relation, from which `Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′` follows by update permute, - so the IH applies, giving us `Γ , x′ ∶ A′ ⊢ N′ [ x ∶= V ] ∶ B′` - By `⇒-I`, we have `Γ ⊢ λ[ x′ ∶ A′ ] (N′ [ x ∶= V ]) ∶ A′ ⇒ B′` + so the IH applies, giving us `Γ , x′ ∶ A′ ⊢ N′ [ x := V ] ∶ B′` + By `⇒-I`, we have `Γ ⊢ λ[ x′ ∶ A′ ] (N′ [ x := V ]) ∶ A′ ⇒ B′` and the definition of substitution (noting `x ≢ x′`) gives - `Γ ⊢ (λ[ x′ ∶ A′ ] N′) [ x ∶= V ] ∶ A′ ⇒ B′` as required. + `Γ ⊢ (λ[ x′ ∶ A′ ] N′) [ x := V ] ∶ A′ ⇒ B′` as required. - If `N` is an application `L′ · M′`, the result follows straightforwardly from the definition of substitution and the induction hypotheses. - - The remaining cases are similar to the application case. + - The remaining cases are similar to application. -We need a couple of lemmas. A closed term can be weakened to any context, and just is injective. -
{% raw %}
-
+
+weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∶ A → Γ ⊢ V ∶ A
 weaken-closed {V} {A} {Γ} ⊢V = contextLemma Γ~Γ′ ⊢V
   where
   Γ~Γ′ : ∀ {x} → x ∈ V → ∅ x ≡ Γ x
+  Γ~Γ′ {x} x∈V = ⊥-elim (x∉V x∈V)
+    where
+    x∉V : ¬ (x ∈ V)
+    x∉V = ∅⊢-closed ⊢V {x}
+
+just-injective : ∀ {X : Set} {x y : X} → _≡_ {A = Maybe X} (just x) (just y) → x ≡ y
+just-injective refl = refl
+
+
+ +
+
+preservation-[:=] {Γ} {x} {A} (Ax {Γ,x∶A} {x′} {B} [Γ,x∶A]x′≡B) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite just-injective [Γ,x∶A]x′≡B  =  weaken-closed ⊢V
+...| no  x≢x′  =  Ax [Γ,x∶A]x′≡B
+preservation-[:=] {Γ} {x} {A} {λ[ x′ ∶ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite x≡x′ = contextLemma Γ′~Γ (⇒-I ⊢N′)
+  where
+  Γ′~Γ : ∀ {y} → y ∈ : ∀(λ[ {x}x′ →∶ xA′ ∈] V N′→) ∅→ x ≡ (Γ x, x′
-  Γ~Γ′ ∶ A) y {x}≡ Γ x∈Vy
+  Γ′~Γ = ⊥-elim{y} (x∉Vfree-λ x∈Vx′≢y y∈N′) with x′ ≟ y
-    where
-    x∉V...| : ¬ (x ∈ V)
-    x∉Vyes x′≡y  = ∅⊢-closed⊥-elim ⊢V(x′≢y {x}x′≡y)
+  ...| no  _     = refl
-
 just-injective...| : ∀ {X : Set} {x y : X}no  x≢x′ →= _≡_⇒-I {A =⊢N′V
+  where
+  x′x⊢N′ Maybe: X}Γ (just, x)x′ (just∶ y) → xA′ ≡, y
-just-injective refl = refl
-{% endraw %}
- -
{% raw %}
-preservation-[∶=] {_} {x ∶ A ⊢ N′ ∶ B′
+  x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′
+  ⊢N′V }: (AxΓ {_}, x′ {x′}∶ [Γ,x∶A]x′≡BA′) ⊢ N′ [ x := V ] ∶ B′
+  ⊢N′V = preservation-[:=] x′x⊢N′ ⊢V with x ≟ x′
 ...| yes x≡x′ rewrite just-injective [Γ,x∶A]x′≡Bpreservation-[:=]  =  weaken-closed (⇒-E ⊢L ⊢M) ⊢V
-...| no  x≢x′  =  Ax [Γ,x∶A]x′≡B⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V)
 preservation-[∶=] {Γ} {x} {A} {λ[ x′preservation-[:=] ∶ A′𝔹-I₁ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with= x ≟ x′𝔹-I₁
 ...|preservation-[:=] yes𝔹-I₂ x≡x′⊢V rewrite x≡x′ = contextLemma𝔹-I₂
+preservation-[:=] Γ′~Γ (⇒-I𝔹-E ⊢N′⊢L ⊢M ⊢N) ⊢V =
   where
-  Γ′~Γ𝔹-E :(preservation-[:=] ∀⊢L {y}⊢V) → y ∈(preservation-[:=] (λ[⊢M x′⊢V) ∶ A′ ] N′) → (Γpreservation-[:=] ,⊢N x′ ∶ A⊢V) y ≡ Γ y
-  Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ ≟ y
-  ...| yes x′≡y  = ⊥-elim (x′≢y x′≡y)
-  ...| no  _     = refl
-...| no  x≢x′ = ⇒-I ⊢N′V
-  where
-  x′x⊢N′ : Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′
-  x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′
-  ⊢N′V : (Γ , x′ ∶ A′) ⊢ N′ [ x ∶= V ] ∶ B′
-  ⊢N′V = preservation-[∶=] x′x⊢N′ ⊢V
-preservation-[∶=] (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (preservation-[∶=] ⊢L ⊢V) (preservation-[∶=] ⊢M ⊢V)
-preservation-[∶=] 𝔹-I₁ ⊢V = 𝔹-I₁
-preservation-[∶=] 𝔹-I₂ ⊢V = 𝔹-I₂
-preservation-[∶=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V =
-  𝔹-E (preservation-[∶=] ⊢L ⊢V) (preservation-[∶=] ⊢M ⊢V) (preservation-[∶=] ⊢N ⊢V)
-{% endraw %}
+ + ### Main Theorem @@ -6316,605 +6361,1155 @@ term `M` has type `A` and takes a step to `N`, then `N` is also a closed term with type `A`. In other words, small-step reduction preserves types. -
{% raw %}
-
+
+preservation : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹ N → ∅ ⊢ N ∶ A
-{% endraw %}
-_Proof_: By induction on the derivation of `\vdash t : T`. + -- We can immediately rule out `var`, `abs`, `T_True`, and - `T_False` as the final rules in the derivation, since in each of - these cases `t` cannot take a step. +_Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`. -- If the last rule in the derivation was `app`, then `t = t_1 - t_2`. There are three cases to consider, one for each rule that - could have been used to show that `t_1 t_2` takes a step to `t'`. +- We can immediately rule out `Ax`, `⇒-I`, `𝔹-I₁`, and + `𝔹-I₂` as the final rules in the derivation, since in each of + these cases `M` cannot take a step. - - If `t_1 t_2` takes a step by `Sapp1`, with `t_1` stepping to - `t_1'`, then by the IH `t_1'` has the same type as `t_1`, and - hence `t_1' t_2` has the same type as `t_1 t_2`. +- If the last rule in the derivation was `⇒-E`, then `M = L · M`. + There are three cases to consider, one for each rule that + could have been used to show that `L · M` takes a step to `N`. - - The `Sapp2` case is similar. + - If `L · M` takes a step by `ξ·₁`, with `L` stepping to + `L′`, then by the IH `L′` has the same type as `L`, and + hence `L′ · M` has the same type as `L · M`. - - If `t_1 t_2` takes a step by `Sred`, then `t_1 = - \lambda x:t_{11}.t_{12}` and `t_1 t_2` steps to ``x∶=t_2`t_{12}`; the - desired result now follows from the fact that substitution - preserves types. + - The `ξ·₂` case is similar. - - If the last rule in the derivation was `if`, then `t = if t_1 - then t_2 else t_3`, and there are again three cases depending on - how `t` steps. + - If `L · M` takes a step by `β⇒`, then `L = λ[ x ∶ A ] N` and `M + = V` and `L · M` steps to `N [ x := V]`; the desired result now + follows from the fact that substitution preserves types. - - If `t` steps to `t_2` or `t_3`, the result is immediate, since - `t_2` and `t_3` have the same type as `t`. +- If the last rule in the derivation was `if`, then `M = if L + then M else N`, and there are again three cases depending on + how `if L then M else N` steps. - - Otherwise, `t` steps by `Sif`, and the desired conclusion + - If it steps via `β𝔹₁` or `βB₂`, the result is immediate, since + `M` and `N` have the same type as `if L then M else N`. + + - Otherwise, `L` steps by `ξif`, and the desired conclusion follows directly from the induction hypothesis. -
{% raw %}
-preservation (Ax x₁) ()
-preservation (⇒-I ⊢N) ()
-preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[∶=] ⊢N ⊢V
-preservation (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L L⟹L′
-...| ⊢L′ = ⇒-E ⊢L′ ⊢M
-preservation (⇒-E ⊢L ⊢M) (γ⇒₂ valueL M⟹M′) with preservation ⊢M M⟹M′
-...| ⊢M′ = ⇒-E ⊢L ⊢M′
-preservation 𝔹-I₁ ()
-preservation 𝔹-I₂ ()
-preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) β𝔹₁ = ⊢M
-preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) β𝔹₂ = ⊢N
-preservation (𝔹-E ⊢L ⊢M ⊢N) (γ𝔹 L⟹L′) with preservation ⊢L L⟹L′
-...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
-{% endraw %}
+
+
+preservation (Ax Γx≡A) ()
+preservation (⇒-I ⊢N) ()
+preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = preservation-[:=] ⊢N ⊢V
+preservation (⇒-E ⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ = ⇒-E ⊢L′ ⊢M
+preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL M⟹M′) with preservation ⊢M M⟹M′
+...| ⊢M′ = ⇒-E ⊢L ⊢M′
+preservation 𝔹-I₁ ()
+preservation 𝔹-I₂ ()
+preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-true = ⊢M
+preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N
+preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
+...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
+
+
-Proof with eauto. - remember (@empty ty) as Gamma. - intros t t' T HT. generalize dependent t'. - induction HT; - intros t' HE; subst Gamma; subst; - try solve `inversion HE; subst; auto`. - - (* app - inversion HE; subst... - (* Most of the cases are immediate by induction, - and `eauto` takes care of them - + (* Sred - apply substitution_preserves_typing with t_{11}... - inversion HT_1... -Qed. #### Exercise: 2 stars, recommended (subject_expansion_stlc) -An exercise in the [Stlc]({{ "Stlc" | relative_url }}) chapter asked about the + +An exercise in the [Types]({{ "Types" | relative_url }}) chapter asked about the subject expansion property for the simple language of arithmetic and boolean expressions. Does this property hold for STLC? That is, is it always the case -that, if `t ==> t'` and `has_type t' T`, then `empty \vdash t : T`? If -so, prove it. If not, give a counter-example not involving conditionals. - +that, if `M ==> N` and `∅ ⊢ N ∶ A`, then `∅ ⊢ M ∶ A`? It is easy to find a +counter-example with conditionals, find one not involving conditionals. ## Type Soundness #### Exercise: 2 stars, optional (type_soundness) + Put progress and preservation together and show that a well-typed term can _never_ reach a stuck state. -Definition stuck (t:tm) : Prop := - (normal_form step) t /\ ~ Value t. +
 
-Corollary soundness : forall t t' T,
-  empty \vdash t : T →
-  t ==>* t' →
-  ~(stuck t').
-Proof.
-  intros t t' T Hhas_type Hmulti. unfold stuck.
-  intros `Hnf Hnot_val`. unfold normal_form in Hnf.
-  induction Hmulti.
+Normal : Term → Set
+Normal M = ∀ {N} → ¬ (M ⟹ N)
+
+Stuck : Term → Set
+Stuck M = Normal M × ¬ Value M
+
+postulate
+  Soundness : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹* N → ¬ (Stuck N)
+
+
+ + ## Uniqueness of Types