checked derivations work with C-R

src/Stlc.lagda

@@ -85,16 +85,16 @@ infix 10 _⟹_
 data _⟹_ : Term → Term → Set where
   β⇒ : ∀ {x A N V} → Value V →
     (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ]
-  γ⇒₀ : ∀ {L L' M} →
+  γ⇒₁ : ∀ {L L' M} →
     L ⟹ L' →
     L · M ⟹ L' · M
-  γ⇒₁ : ∀ {V M M'} →
+  γ⇒₂ : ∀ {V M M'} →
     Value V →
     M ⟹ M' →
     V · M ⟹ V · M'
-  β𝔹₀ : ∀ {M N} →
-    if true then M else N ⟹ M
   β𝔹₁ : ∀ {M N} →
+    if true then M else N ⟹ M
+  β𝔹₂ : ∀ {M N} →
     if false then M else N ⟹ N
   γ𝔹 : ∀ {L L' M N} →
     L ⟹ L' →    
@@ -133,32 +133,32 @@ _∎ : ∀ M → M ⟹* M
 M ∎  =  ⟨⟩
 \end{code}
 
-## Example reductions
+## Example reduction derivations
 
 \begin{code}
-example₀ : not · true ⟹* false
-example₀ =
+reduction₁ : not · true ⟹* false
+reduction₁ =
     not · true
   ⟹⟨ β⇒ value-true ⟩
     if true then false else true
-  ⟹⟨ β𝔹₀ ⟩
+  ⟹⟨ β𝔹₁ ⟩
     false
   ∎
 
-example₁ : two · not · true ⟹* true
-example₁ =
+reduction₂ : two · not · true ⟹* true
+reduction₂ =
     two · not · true
-  ⟹⟨ γ⇒₀ (β⇒ value-λ) ⟩
+  ⟹⟨ γ⇒₁ (β⇒ value-λ) ⟩
     (λ[ x ∶ 𝔹 ] not · (not · var x)) · true
   ⟹⟨ β⇒ value-true ⟩
     not · (not · true)
-  ⟹⟨ γ⇒₁ value-λ (β⇒ value-true) ⟩
+  ⟹⟨ γ⇒₂ value-λ (β⇒ value-true) ⟩
     not · (if true then false else true)
-  ⟹⟨ γ⇒₁ value-λ β𝔹₀ ⟩
+  ⟹⟨ γ⇒₂ value-λ β𝔹₁ ⟩
     not · false
   ⟹⟨ β⇒ value-false ⟩
     if false then false else true
-  ⟹⟨ β𝔹₁ ⟩
+  ⟹⟨ β𝔹₂ ⟩
     true
   ∎
 \end{code}
@@ -182,9 +182,9 @@ data _⊢_∶_ : Context → Term → Type → Set where
     Γ ⊢ L ∶ A ⇒ B →
     Γ ⊢ M ∶ A →
     Γ ⊢ L · M ∶ B
-  𝔹-I₀ : ∀ {Γ} →
-    Γ ⊢ true ∶ 𝔹
   𝔹-I₁ : ∀ {Γ} →
+    Γ ⊢ true ∶ 𝔹
+  𝔹-I₂ : ∀ {Γ} →
     Γ ⊢ false ∶ 𝔹
   𝔹-E : ∀ {Γ L M N A} →
     Γ ⊢ L ∶ 𝔹 →
@@ -196,40 +196,45 @@ data _⊢_∶_ : Context → Term → Type → Set where
 ## Example type derivations
 
 \begin{code}
-example₂ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
-example₂ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₁ 𝔹-I₀)
+typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
+typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
-example₃ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
-example₃ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
+typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
+typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
 \end{code}
 
 Construction of a type derivation is best done interactively.
 We start with the declaration:
 
-  `example₂ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
-  `example₂ = ?`
+  `typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
+  `typing₁ = ?`
 
 Typing control-L causes Agda to create a hole and tell us its expected type.
 
-  `example₂ = { }0`
+  `typing₁ = { }0`
   `?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
 
 Now we fill in the hole, observing that the outermost term in `not` in a `λ`,
 which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which
 we again specify with a hole.
 
-  `example₂ = ⇒-I { }0`
+  `typing₁ = ⇒-I { }0`
   `?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹`
 
 Again we fill in the hole, observing that the outermost term is now
 `if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes
 three arguments, which we again specify with holes.
 
-  `example₂ = ⇒-I (𝔹-E { }0 { }1 { }2)`
+  `typing₁ = ⇒-I (𝔹-E { }0 { }1 { }2)`
   `?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ 𝔹`
   `?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹`
   `?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹`
 
+Again we fill in the three holes, observing that `var 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 computed with a hole.
+
 Filling in the three holes gives the derivation above.
 
 

src/StlcProp.lagda

@@ -26,28 +26,24 @@ open import Stlc
 
 ## Canonical Forms
 
-As we saw for the simple calculus in the [Stlc]({{ "Stlc" | relative_url }})
-chapter, the first step in establishing basic properties of reduction and types
+As we saw for the simple calculus in Chapter [Types]({{ "Types" | relative_url }}),
+the first step in establishing basic properties of reduction and typing
 is to identify the possible _canonical forms_ (i.e., well-typed closed values)
-belonging to each type.  For `bool`, these are the boolean values `true` and
-`false`.  For arrow types, the canonical forms are lambda-abstractions. 
+belonging to each type.  For function types the canonical forms are lambda-abstractions,
+while for boolean types they are values `true` and `false`.  
 
 \begin{code}
 data canonical_for_ : Term → Type → Set where
   canonical-λ : ∀ {x A N B} → canonical (λ[ x ∶ A ] N) for (A ⇒ B)
   canonical-true : canonical true for 𝔹
   canonical-false : canonical false for 𝔹
-  
--- canonical_for_ : Term → Type → Set
--- canonical L for 𝔹       = L ≡ true ⊎ L ≡ false
--- canonical L for (A ⇒ B) = ∃₂ λ x N → L ≡ λ[ x ∶ A ] N
 
 canonicalFormsLemma : ∀ {L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A
 canonicalFormsLemma (Ax ⊢x) ()
-canonicalFormsLemma (⇒-I ⊢N) value-λ = canonical-λ      -- _ , _ , refl
+canonicalFormsLemma (⇒-I ⊢N) value-λ = canonical-λ
 canonicalFormsLemma (⇒-E ⊢L ⊢M) ()
-canonicalFormsLemma 𝔹-I₁ value-true = canonical-true    -- inj₁ refl
-canonicalFormsLemma 𝔹-I₂ value-false = canonical-false  -- inj₂ refl
+canonicalFormsLemma 𝔹-I₁ value-true = canonical-true
+canonicalFormsLemma 𝔹-I₂ value-false = canonical-false
 canonicalFormsLemma (𝔹-E ⊢L ⊢M ⊢N) ()
 \end{code}
 
@@ -62,9 +58,9 @@ progress : ∀ {M A} → ∅ ⊢ M ∶ A → Value M ⊎ ∃ λ N → M ⟹ N
 \end{code}
 
 The proof is a relatively
-straightforward extension of the progress proof we saw in the
-[Types]({{ "Types" | relative_url }}) chapter.
-We'll give the proof in English
+straightforward extension of the progress proof we saw in
+[Types]({{ "Types" | relative_url }}).
+We give the proof in English
 first, then the formal version.
 
 _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
@@ -72,26 +68,26 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
   - The last rule of the derivation cannot be `var`,
     since a variable is never well typed in an empty context.
 
-  - The `true`, `false`, and `abs` cases are trivial, since in
-    each of these cases we can see by inspecting the rule that `t`
-    is a value.
+  - The `λ`, `true`, and `false` cases are trivial, since in
+    each of these cases we can see by inspecting the rule that
+    the term is a value.
 
-  - If the last rule of the derivation is `app`, then `t` has the
-    form `t_1\;t_2` for som e`t_1` and `t_2`, where we know that
-    `t_1` and `t_2` are also well typed in the empty context; in particular,
-    there exists a type `B` such that `\vdash t_1 : A\to T` and
-    `\vdash t_2 : B`.  By the induction hypothesis, either `t_1` is a
+  - If the last rule of the derivation is `⇒-E`, then the term has the
+    form `L · M` for some `L` and `M`, where we know that
+    `L` and `M` are also well typed in the empty context; in particular,
+    there exists types `A` and `B` such that `∅ ⊢ L ∶ A ⇒ B` and
+    `∅ ⊢ M ∶ A`.  By the induction hypothesis, either `L` is a
     value or it can take a reduction step.
 
-  - If `t_1` is a value, then consider `t_2`, which by the other
-    induction hypothesis must also either be a value or take a step.
+    - If `L` is a value, then consider `M`, which by the other
+      induction hypothesis must also either be a value or take a step.
 
-    - Suppose `t_2` is a value.  Since `t_1` is a value with an
-      arrow type, it must be a lambda abstraction; hence `t_1\;t_2`
-      can take a step by `red`.
+      - Suppose `M` is a value.  Since `L` is a value with a
+        function type, it must be a lambda abstraction;
+        hence `L · M` can take a step by `β⇒`.
 
-    - Otherwise, `t_2` can take a step, and hence so can `t_1\;t_2`
-      by `app2`.
+      - Otherwise, `M` can take a step to `M′`, and hence so
+        can `L · M` by `γ⇒₂`.
 
   - If `t_1` can take a step, then so can `t_1 t_2` by `app1`.