completed preservation

src/plta/PandP.lagda

@@ -271,8 +271,10 @@ Let's unpack the first three cases.
       abstraction.  We also have evidence that `M` is
       a value, so our original term steps by `β-ƛ·`.
 
-The remaining cases, for zero, successor, case, and fixpoint,
+The remaining cases are similar.  If by induction we have a
-are similar.
+`step` case we apply a `ξ` rule, and if we have a `done` case
+then either we have a value or apply a `β` rule.  For fixpoint,
+no induction is required as the `β` rule applies immediately.
 
 Our code reads neatly in part because we consider the
 `step` option before the `done` option. We could, of course,
@@ -326,12 +328,15 @@ In symbols,
     -----------------------
     Γ ⊢ M ⦂ A  →  Δ ∋ M ⦂ A
 
-Special cases of renaming include _weakening_ (where `Δ` is an
+Special cases of renaming include the _weaken_ lemma (a term
-extension of `Γ`) and _swapping_ (reordering the occurrence of
+well-typed in the empty context is also well-typed in an arbitary
-variables in `Γ` and `Δ`).  Our renaming lemma is similar to the
+context) the _drop_ lemma (a term well-typed in a context where the
-_context invariance_ lemma in _Software Foundations_, but does not
+same variable appears twice remains well-typed if we drop the shadowed
-require a separate definition of the `appears_free_in` relation
+occurrence) and the _swap_ lemma (a term well-typed in a context
-which is needed there.
+remains well-typed if we swap two variables).  Renaming is similar to
+the _context invariance_ lemma in _Software Foundations_, but it does
+not require the definition of `appears_free_in` nor the
+`free_in_context` lemma.
 
 The second step is to show that types are preserved by
 _substitution_.
@@ -375,10 +380,10 @@ We now proceed with our three-step programme.
 
 ## Renaming
 
-We often need to "rebase" a type derivation, replacing a
+We often need to "rebase" a type derivation, replacing a derivation
-derivation `Γ ⊢ M ⦂ A` by a related derivation `Δ ⊢ M ⦂ A`.
+`Γ ⊢ M ⦂ A` by a related derivation `Δ ⊢ M ⦂ A`.  We may do so as long
-We may do so as long as every variable that appears in
+as every variable that appears in `Γ` also appears in `Δ`, and with
-`Γ` also appears in `Δ`, and with the same type.
+the same type.
 
 Three of the rules for typing (lambda abstraction, case on naturals,
 and fixpoint) have hypotheses that extend the context to include a
@@ -405,18 +410,19 @@ ext ρ (S x≢y ∋x)  =  S x≢y (ρ ∋x)
 Let `ρ` be the name of the map that takes evidence that
 `x` appears in `Γ` to evidence that `x` appears in `Δ`.
 The proof is by induction on the evidence that `x` appears
-in the extended map `Γ , y ⦂ B`. If `x` is the same as `y`,
+in the extended map `Γ , y ⦂ B`.
-we used `Z` to access the last variable in the extended `Γ`;
-and can similarly use `Z` to access the last variable in the
-extended `Δ`.  If `x` differs from `y`, then we used `S`
-to skip over the last variable in the extended `Γ`, where
-`x≢y` is evidence that `x` and `y` differ, and `∋x` is the
-evidence that `x` appears in `Γ`; and we can similarly use
-`S` to skip over the last variable in the extended `Δ`,
-applying `ρ` to find the evidence that `w` appears
-in `Δ`.
 
-With this lemma under our belts, it is straightforward to
+* If `x` is the same as `y`, we used `Z` to access the last variable
+in the extended `Γ`; and can similarly use `Z` to access the last
+variable in the extended `Δ`.
+
+* If `x` differs from `y`, then we used `S` to skip over the last
+variable in the extended `Γ`, where `x≢y` is evidence that `x` and `y`
+differ, and `∋x` is the evidence that `x` appears in `Γ`; and we can
+similarly use `S` to skip over the last variable in the extended `Δ`,
+applying `ρ` to find the evidence that `w` appears in `Δ`.
+
+With the extension lemma under our belts, it is straightforward to
 prove renaming preserves types.
 \begin{code}
 rename : ∀ {Γ Δ}
@@ -441,29 +447,30 @@ that the variable appears in `Γ` yields the corresponding evidence that
 the variable appears in `Δ`.
 
 * If the term is a lambda abstraction, use the previous lemma to
-extend the map `ρ` suitably and recursively rename the body of the
+extend the map `ρ` suitably and use induction to rename the body of the
 abstraction
 
-* If the term is an application, recursively rename both the
+* If the term is an application, use induction to rename both the
 function and the argument.
 
-The remaining cases, for zero, successor, case, and fixpoint, are
+The remaining cases are similar, using induction for each subterm, and
-similar.  In case and fixpoint, as with lambda abstraction, map `ρ`
+also extension where the construct introduces a bound variable.
-needs to be extended to account for the bound variable.  The induction
+
-is over the derivation that the term is well-typed, so the extension
+The induction is over the derivation that the term is well-typed,
-doesn't invalidate the inductive hypothesis. Equivalently, the
+so extending the context doesn't invalidate the inductive hypothesis.
-recursion terminates because the second argument is always smaller,
+Equivalently, the recursion terminates because the second argument
-even though the first argument sometimes grows larger.
+always grows smaller, even though the first argument sometimes grows larger.
 
 We have three important corollaries, each proved by constructing
-a suitable map between contexts.  First,
+a suitable map between contexts.
-any closed term can be weakened to any context.
+
+First, a closed term can be weakened to any context.
 \begin{code}
-rename-∅ : ∀ {Γ M A}
+weaken : ∀ {Γ M A}
   → ∅ ⊢ M ⦂ A
     ----------
   → Γ ⊢ M ⦂ A
-rename-∅ {Γ} ⊢M = rename ρ ⊢M
+weaken {Γ} ⊢M = rename ρ ⊢M
   where
   ρ : ∀ {z C}
     → ∅ ∋ z ⦂ C
@@ -474,14 +481,14 @@ rename-∅ {Γ} ⊢M = rename ρ ⊢M
 Here the map `ρ` is trivial, since there are no possible
 arguments in the empty context `∅`.
 
-Second, if the last two variables in a context are
+Second, if the last two variables in a context are equal then we can
-equal, the term can be renamed to drop the redundant one.
+drop the shadowed one.
 \begin{code}
-rename-≡ : ∀ {Γ x M A B C}
+drop : ∀ {Γ x M A B C}
   → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C
     --------------------------
   → Γ , x ⦂ B ⊢ M ⦂ C
-rename-≡ {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
+drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
   where
   ρ : ∀ {z C}
     → Γ , x ⦂ A , x ⦂ B ∋ z ⦂ C
@@ -498,15 +505,14 @@ first position can only happen if the variable looked for differs from
 found in the second position, which also contains `x`, this leads to a
 contradiction (evidenced by `x≢x refl`).
 
-Third, if the last two variables in a context differ,
+Third, if the last two variables in a context differ then we can swap them.
-the term can be renamed to flip their order.
 \begin{code}
-rename-≢ : ∀ {Γ x y M A B C}
+swap : ∀ {Γ x y M A B C}
   → x ≢ y
   → Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C
     --------------------------
   → Γ , x ⦂ A , y ⦂ B ⊢ M ⦂ C
-rename-≢ {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
+swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
   where
   ρ : ∀ {z C}
     → Γ , y ⦂ B , x ⦂ A ∋ z ⦂ C
@@ -549,28 +555,28 @@ subst : ∀ {Γ x N V A B}
     --------------------
   → Γ ⊢ N [ x := V ] ⦂ B
 subst {x = y} ⊢V (Ax {x = x} Z) with x ≟ y
-... | yes refl     =  rename-∅ ⊢V
+... | yes refl     =  weaken ⊢V
 ... | no  x≢y      =  ⊥-elim (x≢y refl)
 subst {x = y} ⊢V (Ax {x = x} (S x≢y ∋x)) with x ≟ y
 ... | yes refl     =  ⊥-elim (x≢y refl)
 ... | no  _        =  Ax ∋x
 subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
-... | yes refl     =  ⊢ƛ (rename-≡ ⊢N)
+... | yes refl     =  ⊢ƛ (drop ⊢N)
-... | no  x≢y      =  ⊢ƛ (subst ⊢V (rename-≢ x≢y ⊢N))
+... | no  x≢y      =  ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
 subst ⊢V (⊢L · ⊢M) = subst ⊢V ⊢L · subst ⊢V ⊢M
 subst ⊢V ⊢zero     =  ⊢zero
 subst ⊢V (⊢suc ⊢M) =  ⊢suc (subst ⊢V ⊢M)
 subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y
-... | yes refl     =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (rename-≡ ⊢N)
+... | yes refl     =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N)
-... | no  x≢y      =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (rename-≢ x≢y ⊢N))
+... | no  x≢y      =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N))
 subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y
-... | yes refl     =  ⊢μ (rename-≡ ⊢M)
+... | yes refl     =  ⊢μ (drop ⊢M)
-... | no  x≢y      =  ⊢μ (subst ⊢V (rename-≢ x≢y ⊢M))
+... | no  x≢y      =  ⊢μ (subst ⊢V (swap x≢y ⊢M))
 \end{code}
 We induct on the evidence that `N` is well-typed in the
 context `Γ` extended by `x`.
 
-Immediately, we note a wee issue with naming.  In the lemma
+First, we note a wee issue with naming.  In the lemma
 statement, the variable `x` is an implicit parameter for the variable
 substituted, while in the type rules for variables, abstractions,
 cases, and fixpoints, the variable `x` is an implicit parameter for
@@ -583,68 +589,7 @@ definition of substitution in the previous chapter.  The proof never
 mentions the types of `x`, `y`, `V`, or `N`, so in what follows we
 choose type name as convenient.
 
-Now let's unpack the first three cases.
+Now that naming is resolved, let's unpack the first three cases.
-
-* In the variable case, given `∅ ⊢ V ⦂ B` and `Γ , y ⦂ B ⊢ ⌊ x ⌋ ⦂ A`,
-  we need to show `Γ ⊢ x [ y := V ] ⦂ A`.  There are two subcases,
-  depending on the evidence demonstrating `Γ , y ⦂ B ∋ x ⦂ A`.
-
-  + If `x` appears at the end of the context, as evidenced by `Z`,
-    then `x` and `y` are necessarily identical, as are `A` and `B`.
-    Nonetheless, we must evaluate `x ≟ y` in order to allow the
-    definition of substitution to simplify.
-
-    - If the variables are equal, then `x [ x := V ]` simplifies to
-      `V`, and the weakening lemma `rename-∅` applied to evidence of 
-      `∅ ⊢ V ⦂ A` yields evidence that `Γ ⊢ V ⦂ A`, as required.
- 
-    - If the variables are unequal, we have a contradiction and the
-      result follows immediately by `⊥-elim`.
-
-  + If `x` appears elsewhere in the context, as evidenced by `S x≢y
-    ∋x`, then `x` and `y` are necessarily distinct.  Nonetheless, we
-    must again evaluate `x ≟ y` in order to allow the definition of
-    substitution to simplify.
-
-    - If the variables are equal, we have a contradiction and the
-      result follows immediately by `⊥-elim`.
-
-    - If the variables are unequal, then `x [ y := V ]` simplifies to
-      `x`, and `∋x` provides evidence that `Γ ∋ x ⦂ A`, as required.
-
-* In the abstraction case, given `∅ ⊢ V ⦂ B` and `Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C`
-  we need to show `Γ ⊢ (ƛ x ⇒ N) [ y := V ] ⦂ A ⇒ C`.  We evaluate `x ≟ y` in
-  order to allow the definition of substitution to simplify.
-
-  + If the variables are equal, then `(ƛ x ⇒ N) [ x := V ]` simplifies
-    to `ƛ x ⇒ N`, and the drop lemma `rename-≡` applied to evidence of
-    `Γ , x ⦂ B , x ⦂ A ⊢ N ⦂ C` yields evidence that `Γ , x ⦂ A ⊢ N ⦂ C`.
-    The typing rule for abstractions then yields `Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ C`,
-    as required.
-
-
-  + If the variables are unequal, then `(ƛ x ⇒ N) [ y := V ]` simplifies
-    to `ƛ x ⇒ (N [ y := V ])`.  The swap lemma `rename-≢` applied to
-    evidence of `Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C` yields evidence that
-    `Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C`, which allows us to apply the inductive
-    hypothesis to conclude `Γ , x ⦂ A ⊢ N [ y := V ] ⦂ C`. By the typing
-    rule for abstactions we then have `Γ ⊢ ƛ x ⇒ (N [ y := V ]) ⦂ A ⇒ C`,
-    as required.
-
-* In the application case, given `∅ ⊢ V ⦂ C` and `Γ , y ⦂ C ⊢ L ⦂ A ⇒ B` and
-  `Γ , y ⦂ C ⊢ M ⦂ A`.  Applying the induction hypothesis to `L` and `M`
-  `Γ ⊢ L [ y := V ] ⦂ A ⇒ B` and `Γ ⊢ M [ y := V ] ⦂ A`.  By the typing rule
-  for applications we then have `Γ ⊢ (L · M) [ y := V ] ⦂ B` as required.
-
-The remaining cases, for zero, successor, case, and fixpoint,
-are similar.
-
-
----
-
-revised attempt
-
----
 
 * In the variable case, we must show
 
@@ -653,31 +598,42 @@ revised attempt
     ------------------------
     Γ ⊢ ⌊ x ⌋ [ y := V ] ⦂ A
 
-  There are two subcases, depending on the evidence demonstrating
+  where the second hypothesis follows from:
-  `Γ , y ⦂ B ∋ x ⦂ A`.
 
-  + If `x` appears at the end of the context, as evidenced by `Z`,
+    Γ , y ⦂ B ∋ x ⦂ A
-    then `x` and `y` are necessarily identical, as are `A` and `B`.
+    
-    Nonetheless, we must evaluate `x ≟ y` in order to allow the
+  There are two subcases, depending on the evidence for this judgement.
-    definition of substitution to simplify.
+
+  + The lookup judgement is evidenced by rule `Z`:
+
+       -----------------
+       Γ , x ⦂ A ⊢ x ⦂ A
+
+    In this case, `x` and `y` are necessarily identical, as are `A`
+    and `B`.  Nonetheless, we must evaluate `x ≟ y` in order to allow
+    the definition of substitution to simplify.
 
     - If the variables are equal, then after simplification we
       must show
 
         ∅ ⊢ V ⦂ A
-        Γ , x ⦂ A ⊢ ⌊ x ⌋ ⦂ A
+        ---------
-        ------------------------
         Γ ⊢ V ⦂ A
 
-      The first hypothesis implies the conclusion by the weakening
+      which follows by weakening.
-      lemma `rename-∅`.
 
     - If the variables are unequal we have a contradiction.
 
-  + If `x` appears elsewhere in the context, as evidenced by `S x≢y ∋x`,
+  + The lookup judgement is evidenced by rule `S`:
-    then `x` and `y` are necessarily distinct.  Nonetheless, we
+
-    must again evaluate `x ≟ y` in order to allow the definition of
+       x ≢ y
-    substitution to simplify.
+       Γ ∋ x ⦂ A
+       -----------------
+       Γ , y ⦂ B ∋ x ⦂ A
+
+    In this case, `x` and `y` are necessarily distinct.
+    Nonetheless, we must again evaluate `x ≟ y` in order to allow
+    the definition of substitution to simplify.
 
     - If the variables are equal we have a contradiction.
 
@@ -685,19 +641,25 @@ revised attempt
       must show
 
         ∅ ⊢ V ⦂ B
-        Γ , y ⦂ B ⊢ ⌊ x ⌋ ⦂ A
+        x ≢ y
-        ------------------------
+        Γ ∋ x ⦂ A
+        -------------
         Γ ⊢ ⌊ x ⌋ ⦂ A
 
-      This follows immediately, since `∋x` provides evidence that `Γ ∋ x ⦂ A`.
+      which follows by the typing rule for variables.
+      
 
 * In the abstraction case, we must show
 
     ∅ ⊢ V ⦂ B
-    Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
+    Γ , y ⦂ B ⊢ (ƛ x ⇒ N) ⦂ A ⇒ C
     --------------------------------
     Γ ⊢ (ƛ x ⇒ N) [ y := V ] ⦂ A ⇒ C
 
+  where the second hypothesis follows from
+
+    Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
+
   We evaluate `x ≟ y` in order to allow the definition of substitution to simplify.
 
   + If the variables are equal then after simplification we must show
@@ -707,7 +669,7 @@ revised attempt
       -------------------------
       Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ C
 
-    From the drop lemma, `rename-≡`, we may conclude
+    From the drop lemma, `drop`, we may conclude
 
       Γ , x ⦂ B , x ⦂ A ⊢ N ⦂ C
       -------------------------
@@ -722,7 +684,7 @@ revised attempt
       --------------------------------
       Γ ⊢ ƛ x ⇒ (N [ y := V ]) ⦂ A ⇒ C
 
-    From the swap lemma, `rename-≢`, we may conclude
+    From the swap lemma we may conclude
 
       Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
       -------------------------
@@ -740,23 +702,30 @@ revised attempt
 * In the application case, we must show
 
     ∅ ⊢ V ⦂ C
+    Γ , y ⦂ C ⊢ L · M ⦂ B
+    --------------------------
+    Γ ⊢ (L · M) [ y := V ] ⦂ B
+
+  where the second hypothesis follows from the two judgements
+
     Γ , y ⦂ C ⊢ L ⦂ A ⇒ B
     Γ , y ⦂ C ⊢ M ⦂ A
-    ------------------------------
-    Γ ⊢ (L · M) [ y := V ] ⦂ B
 
   By the definition of substitution, we must show
 
-    Γ ⊢ (L [ y := V ]) · (M [ y := V ])
+    ∅ ⊢ V ⦂ C
+    Γ , y ⦂ C ⊢ L ⦂ A ⇒ B
+    Γ , y ⦂ C ⊢ M ⦂ A
+    ---------------------------------------
+    Γ ⊢ (L [ y := V ]) · (M [ y := V ]) ⦂ B
 
   Applying the induction hypothesis for `L` and `M` and the typing
   rule for applications yields the required conclusion.
 
 The remaining cases, for zero, successor, case, and fixpoint,
-are similar.
+are similar.  Case and fixpoint are similar to lambda abstaction,
-
+in that we need to test whether the variables are equal, applying
-
+the drop lemma in one case and the swap lemma in the other.
-
 
 ### Main Theorem
 
@@ -781,6 +750,57 @@ preserve (⊢case ⊢zero ⊢M ⊢N)     β-case-zero      =  ⊢M
 preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-case-suc VV)  =  subst ⊢V ⊢N 
 preserve (⊢μ ⊢M)                 (β-μ)            =  subst (⊢μ ⊢M) ⊢M
 \end{code}
+The proof never mentions the types of `M` or `N`,
+so in what follows we choose type name as convenient.
+
+Let's unpack the cases for two of the reduction rules.
+
+* Rule `ξ-·₁`.  We have
+
+    L ⟶ L′
+    ----------------
+    L · M ⟶ L′ · M
+
+  where the left-hand side is typed by
+
+    Γ ⊢ L ⦂ A ⇒ B
+    Γ ⊢ M ⦂ A
+    -------------
+    Γ ⊢ L · M ⦂ B
+
+  By induction, we have
+
+    Γ ⊢ L ⦂ A ⇒ B
+    L ⟶ L′
+    --------------
+    Γ ⊢ L′ ⦂ A ⇒ B
+
+  from which the typing of the right-hand side follows immediately.
+
+* Rule `β-ƛ·`.  We have
+
+    Value V
+    ----------------------------
+    (ƛ x ⇒ N) · V ⊢ N [ x := V ]
+
+  where the left-hand side is typed by
+
+    Γ , x ⦂ A ⊢ N ⦂ B
+    -------------------
+    Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B    Γ ⊢ V ⦂ A
+    --------------------------------
+    Γ ⊢ (ƛ x ⇒ N) · V ⦂ B
+
+  By the substitution lemma, we have
+
+    Γ ⊢ V ⦂ A
+    Γ , x ⦂ A ⊢ N ⦂ B
+    --------------------
+    Γ ⊢ N [ x := V ] ⦂ B
+
+  from which the typing of the right-hand side follows immediately.
+
+The remaining cases are similar
 
 
 ## Normalisation