From 8658bb1b427c5a47be285126a4d1a87752f61e56 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Mon, 17 Jul 2017 18:09:37 +0100 Subject: [PATCH] finished first draft of Stlc --- out/Maps.md | 446 +- out/Stlc.md | 6725 ++++++++++++++-------------- out/StlcProp.md | 10267 +++++++++++++++++++++---------------------- src/Maps.lagda | 10 + src/Stlc.lagda | 157 +- src/StlcProp.lagda | 10 +- 6 files changed, 9077 insertions(+), 8538 deletions(-) diff --git a/out/Maps.md b/out/Maps.md index eb38d314..62703ef3 100644 --- a/out/Maps.md +++ b/out/Maps.md @@ -32,7 +32,8 @@ much difference, though, because we've been careful to name our own definitions and theorems the same as their counterparts in the standard library, wherever they overlap. -
{% raw %}
+
+
 open)
-{% endraw %}

+
+
Documentation for the standard library can be found at . @@ -229,7 +231,8 @@ maps. For this purpose, we again use the type `Id` from the [Lists](sf/Lists.html) chapter. To make this chapter self contained, we repeat its definition here. -
{% raw %}
+
+
 dataId
-{% endraw %}

+
+
We recall a standard fact of logic. -
{% raw %}
+
+
 contrapositive)
-{% endraw %}

+
+
Using the above, we can decide equality of two identifiers by deciding equality on the underlying strings. -
{% raw %}
+
+
 _≟_refl
-{% endraw %}

+
+
## Total Maps @@ -727,7 +735,8 @@ We build partial maps in two steps. First, we define a type of _total maps_ that return a default value when we look up a key that is not present in the map. -
{% raw %}
+
+
 TotalMapA
-{% endraw %}

+
+
Intuitively, a total map over anfi element type `A` _is_ just a function that can be used to look up ids, yielding `A`s. -
{% raw %}
+
+
 modulewhere
-{% endraw %}

+
+
The function `always` yields a total map given a default element; this map always returns the default element when applied to any id. -
{% raw %}
+
+
   alwaysv
-{% endraw %}

+
+
More interesting is the update function, which (as before) takes a map `ρ`, a key `x`, and a value `v` and returns a new map that takes `x` to `v` and takes every other key to whatever `ρ` does. -
{% raw %}
+
+
   infixly
-{% endraw %}

+
+
This definition is a nice example of higher-order programming. The update function takes a _function_ `ρ` and yields a new @@ -1044,7 +1060,8 @@ function that behaves like the desired map. For example, we can build a map taking ids to naturals, where `x` maps to 42, `y` maps to 69, and every other key maps to 0, as follows: -
{% raw %}
+
+
   modulerefl
-{% endraw %}

+
+
This completes the definition of total maps. Note that we don't need to define a `find` operation because it is just function @@ -1327,7 +1345,8 @@ the lemmas! #### Exercise: 1 star, optional (apply-always) The `always` map returns its default element for all keys: -
{% raw %}
+
+
   postulatev
-{% endraw %}

+
+
#### Exercise: 2 stars, optional (update-eq) @@ -1516,7 +1538,8 @@ Next, if we update a map `ρ` at a key `x` with a new value `v` and then look up `x` in the map resulting from the update, we get back `v`: -
{% raw %}
+
+
   postulatev
-{% endraw %}

+
+
#### Exercise: 2 stars, optional (update-neq) @@ -1853,7 +1879,8 @@ On the other hand, if we update a map `m` at a key `x` and then look up a _different_ key `y` in the resulting map, we get the same result that `m` would have given: -
{% raw %}
+
+
   update-neqrefl
-{% endraw %}

+
+
For the following lemmas, since maps are represented by functions, to show two maps equal we will need to postulate extensionality. -
{% raw %}
+
+
   postulateρ′
-{% endraw %}

+
+
#### Exercise: 2 stars, optional (update-shadow) If we update a map `ρ` at a key `x` with a value `v` and then @@ -2230,7 +2260,8 @@ resulting map behaves the same (gives the same result when applied to any key) as the simpler map obtained by performing just the second update on `ρ`: -
{% raw %}
+
+
   postulate)
-{% endraw %}

+
+
#### Exercise: 2 stars (update-same) @@ -2778,7 +2812,8 @@ Prove the following theorem, which states that if we update a map `ρ` to assign key `x` the same value as it already has in `ρ`, then the result is equal to `ρ`: -
{% raw %}
+
+
   postulateρ
-{% endraw %}

+
+
#### Exercise: 3 stars, recommended (update-permute) @@ -3156,7 +3194,8 @@ Prove one final property of the `update` function: If we update a map `m` at two distinct keys, it doesn't matter in which order we do the updates. -
{% raw %}
+
+
   postulate)
-{% endraw %}

+
+
## Partial maps @@ -4649,7 +4693,8 @@ Finally, we define _partial maps_ on top of total maps. A partial map with elements of type `A` is simply a total map with elements of type `Maybe A` and default element `nothing`. -
{% raw %}
+
+
 PartialMap)
-{% endraw %}

 
-
{% raw %}
+

+
+
+
 modulewhere
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   ∅nothing
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   infixl)
-{% endraw %}

+
+
We now lift all of the basic lemmas about total maps to partial maps. -
{% raw %}
+
+
   apply-∅x
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   update-eq)
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   update-neqx≢y
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   update-shadow)
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   update-samex
-{% endraw %}

 
-
{% raw %}
+

+
+
+
   update-permutex≢y
-{% endraw %}

+
+
+ +We will also need the following basic facts about the `Maybe` type. + +
+
+  just≢nothing : ∀ {X : Set} → ∀ {x : X} → ¬ (_≡_ {A = Maybe X} (just x) nothing)
+  just≢nothing ()
+
+  just-injective : ∀ {X : Set} {x y : X} → _≡_ {A = Maybe X} (just x) (just y) → x ≡ y
+  just-injective refl = refl
+
+
diff --git a/out/Stlc.md b/out/Stlc.md index 069d4a8e..dc5c5960 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -7,7 +7,7 @@ permalink : /Stlc The _lambda-calculus_, first published by the logician Alonzo Church in 1932, is a core calculus with only three syntactic constructs: variables, abstraction, and application. It embodies the concept of -_functional abstraction_, which shows up in almsot every programming +_functional abstraction_, which shows up in almost every programming language in some form (as functions, procedures, or methods). The _simply-typed lambda calculus_ (or STLC) is a variant of the lambda calculus published by Church in 1940. It has just the three @@ -108,162 +108,174 @@ lists, records, subtyping, and mutable state. >∅); renaming (_,_↦_just-injective) torenaming (_,_↦_ to _,_∶_) open import Data.Nat using (ℕ) -open import Data.Nat using (ℕ) +open import Data.Maybe using (Maybe; just; nothing) open import Relation.Nullary using (Dec; yes; no) -open import no; ¬_) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) @@ -289,79 +301,79 @@ And here it is formalised in Agda. 
 
-infixr 20 _⇒_
 
 data Type : Set where
-  _⇒_ : Type: →Set Typewhere → Type
   𝔹_⇒_ : Type → Type → Type
+  𝔹 : Type
 
@@ -382,7 +394,7 @@ and three are for the base type, booleans:
 Abstraction is also called lambda abstraction, and is the construct
 from which the calculus takes its name. 
 
-With the exception of variables, each construct either constructs
+With the exception of variables, each term form either constructs
 a value of a given type (abstractions yield functions, true and
 false yield booleans) or deconstructs it (applications use functions,
 conditionals use booleans). We will see this again when we come
@@ -397,134 +409,113 @@ And here it is formalised in Agda.
 
 
 
-infixl 20 _·_
 infix  15 λ[_∶_]_
 infix  15 if_then_else_
 
 data Term : Set where
   ` : Id → Term
-  λ[_∶_]_ : Id → → Type → Term → Term
   _·_λ[_∶_]_ : Id → Type :→ Term → Term → Term
   _·_ : Term → Term → Term
+  true : Term
-  false : Term Term
   if_then_else_false : Term
+  if_then_else_ →: Term → Term → Term → Term
 
@@ -658,246 +670,246 @@ and applies the function to the boolean twice.
 
 
 
-f x y : Id
-f  =  id 0
- x  =  id 1y : Id
 yf  =  id 20
+x  =  id 1
+y  =  id 2
 
 not two : Term 
-not =  λ[ x ∶: 𝔹 ] (if `Term 
+not x=  λ[ thenx false∶ else𝔹 ] (if true)
-two` =  λ[x fthen ∶false else 𝔹 ⇒ 𝔹true)
+two ] =  λ[ x ∶ 𝔹 ] ` f ·∶ (`𝔹 ⇒ 𝔹 ] fλ[ · ` x ∶ 𝔹 ] ` f · (` f · ` x)
 
@@ -909,21 +921,12 @@ and applies the function to the boolean twice.
 In an abstraction `λ[ x ∶ A ] N` we call `x` the _bound_ variable
 and `N` the _body_ of the abstraction.  One of the most important
 aspects of lambda calculus is that names of bound variables are
-irrelevant.  Thus the two terms
+irrelevant.  Thus the four terms
 
-    λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
-
-and
-
-    λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y)
-
-and 
-
-    λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander)
-
-and even
-
-    λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f)
+* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ``
+* `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) ``
+* `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) ``
+* `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) ``
 
 are all considered equivalent.  This equivalence relation
 is sometimes called _alpha renaming_.
@@ -981,369 +984,369 @@ to be weaker than application. For instance,
 
 
 
-ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡⇒ (𝔹) ⇒ 𝔹) ⇒ (𝔹 ≡ ⇒ (𝔹) ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
 ex₁ = refl
 
 ex₂ : two · not · true ≡· (two · not) · true
-ex₂ ≡ (two · not=) · true
+ex₂ = refl
 
 ex₃ : λ[ f ∶ 𝔹 ⇒ 𝔹: ] λ[ f x∶ ∶𝔹 𝔹⇒ ]𝔹 `] fλ[ ·x (`∶ f𝔹 ·] ` x)
-      ≡f · (` f · (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` x)
+      ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ ·x ∶ 𝔹 ] (` f · ` f · (` f · ` x))))
 ex₃ = refl
 
@@ -1395,130 +1398,130 @@ The predicate `Value M` holds if term `M` is a value.
 
 
 
-data Value : Term → SetValue : Term → Set where
   value-λ     : ∀ {x A     : N}∀ → Value{x (λ[ x ∶ A ] N} → Value (λ[ x ∶ A ] N)
-  value-true  : Value true
   value-false value-true  : Value true
+  value-false : Value false
 
@@ -1591,646 +1594,646 @@ Here is the formal definition in Agda.
 
 
 
-_[_:=_] : Term → Id → Term → Term
 (` x′) [ x := V ]x′) with[ x ≟:= x′
-...V |] with yesx ≟ _ = Vx′
 ... | no  yes _ = ` x′V
 (λ[... | no  _ = ` x′
+(λ[ ∶ A′ ] N′) [x′ x∶ :=A′ V] ]N′) with[ x ≟:= x′
-...V |] with yesx ≟ _ = λ[x′
+... x′| ∶yes A′_ ]= N′λ[ x′ ∶ A′ ] N′
 ... | no  _ = λ[ x′| ∶no A′  _ ]= (N′λ[ [x′ x∶ :=A′ V] ])
-(L′N′ ·[ M′)x := V [ x :=])
+(L′ V· ] M′=)  (L′ [ x := xV := V ]) · =  (M′L′ [ x := xV :=]) V· (M′ [ x := V ])
 (true) [ x := V ] =) true
-(false[ x := V ] )= [ x := V ] = falsetrue
 (iffalse) L′[ x := V ] = thenfalse
+(if M′ elseL′ N′)then [ xM′ := Velse ] N′=)
-  if (L′[ x := V [] x= := V
+  if ])(L′ then[ x (M′:= [V x]) := Vthen ])(M′ else[ x (N′:= [V x]) := Velse (N′ [ x := V ])
 
@@ -2262,666 +2265,666 @@ Here is confirmation that the examples above are correct.
 
 
 
-ex₁₁ : ` f [ f := not: ` ]f ≡[  not f := not ] ≡  not
 ex₁₁ = refl
-
-ex₁₂ := true [ f := not ] ≡ true
-ex₁₂ = refl
 
 ex₁₃ex₁₂ : true [ f := not ] ≡ true
+ex₁₂ := (` f · true) [ f := not ] ≡ not · true
-ex₁₃ = refl
 
 ex₁₄ex₁₃ : (` f · true) [ f := not ] ≡ not · true
+ex₁₃ := (` frefl
+
+ex₁₄ ·: (` f · true)) [(` f :=· not ]true)) ≡[ notf ·:= (not ] ·≡ true)not ·
-ex₁₄ (not =· refltrue)
-
 ex₁₅ex₁₄ := refl
+
+ex₁₅ : (λ[ x ∶ 𝔹 ] ` f · (` f𝔹 ·] ` x))f · [(` f :=· not` ]x)) ≡[ λ[f x:= ∶ 𝔹not ] not≡ ·λ[ (notx ∶ 𝔹 ·] not · (not · ` x)
 ex₁₅ = refl
-
-ex₁₆ := (λ[ y ∶ 𝔹 ] ` y) [ x := true ] ≡ λ[ y ∶ 𝔹 ] ` y
-ex₁₆ = refl
 
 ex₁₇ex₁₆ : (λ[ y ∶ 𝔹 ] ` y) [ x := true ] ≡ λ[ y ∶ 𝔹 ] ` y
+ex₁₆ := refl
+
+ex₁₇ : (λ[ x ∶ 𝔹 ] ` x) [x x∶ := true ] ≡ λ[ x ∶ 𝔹 ] ` x) [ x := true ] `≡ λ[ x
-ex₁₇ ∶ =𝔹 ] ` x
+ex₁₇ = refl
 
@@ -2950,8 +2953,8 @@ conditional, we first reduce the condition until it becomes a value;
 if the condition is true the conditional reduces to the first
 branch and if false it reduces to the second branch.a
 
-In an informal presentation of the formal semantics, the rules
-are written as follows.
+In an informal presentation of the formal semantics, 
+the rules for reduction are written as follows.
 
     L ⟹ L′
     --------------- ξ·₁
@@ -2991,571 +2994,573 @@ a deconstructor, in our case `λ` and `·`, or
 We give them names starting with the Greek letter beta, `β`,
 and indeed such rules are traditionally called beta rules.
 
+Here are the above rules formalised in Agda.
+
 
 
-infix 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
-  ξ·₁ : ∀ {L L′ M} →
-    L ⟹ L′ →
-    L · M ⟹_⟹_ L′ · M
-  ξ·₂ : ∀Term {V→ MTerm → Set M′} →where
-    Valueξ·₁ : ∀ V{L L′ M} →
     M ⟹ M′ →L ⟹ L′ →
     VL · M ⟹ V · M′ L′ · M
   βλ· : ∀ {xξ·₂ A: N∀ {V} →M ValueM′} V →
     (λ[Value V x→ ∶ A ]
+    M N)⟹ ·M′ V→ ⟹ N [
+    V x· :=M ⟹ V ]· M′
   ξif : ∀βλ· : ∀ {Lx L′A M N} V} →
-    L ⟹Value L′V →    
+      >
     if(λ[ Lx then∶ MA else] N) · V ⟹ N ⟹[ ifx L′:= thenV M else N]
   βif-trueξif : ∀ {L L′ M N} →
+    L N} →
-    if true then M else N ⟹ L′ →    
+    if L then M
-  βif-false else N ⟹ if L′ then :M ∀ {Melse N} →
-    ifβif-true false: then∀ {M N} M→ else N
+    if ⟹true then M else N ⟹ M
+  βif-false : ∀ {M N} →
+    if false then M else N ⟹ N
 
@@ -3625,189 +3630,189 @@ Here it is formalised in Agda.
 
 
 
-infix 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : Term → Term → Set where
-  _∎ : ∀ M → M ⟹* M
-  _⟹⟨_⟩_ : ∀ L {M N} → L_⟹*_ ⟹: MTerm → M ⟹* N → LTerm ⟹*→ Set where
+  _∎ : ∀ M → M ⟹* M
+  _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N
 
@@ -3827,477 +3832,477 @@ out example reductions in an appealing way.
 
 
 
-reduction₁ : not · true ⟹* false
 reduction₁ =
     not · true
-  ⟹⟨ βλ· value-true ⟩
-    if true then false else true
-  ⟹⟨ βif-true ⟩
-    falsetrue
   ⟹⟨ βλ· value-true ⟩
+    if true then false else true
+  ⟹⟨ βif-true ⟩
+    false
+  ∎
 
 reduction₂ : two · not · true ⟹* true
-reduction₂ =
-    two · not · true
-  ⟹⟨ ξ·₁ (βλ· value-λ) ⟩
-    (λ[ x· true ⟹* ∶ 𝔹 ] not · (not · ` x)) · true
-  ⟹⟨reduction₂ βλ· value-true ⟩=
     two · not · true
+  ⟹⟨ ξ·₁ (βλ· value-λ) ·⟩ (not · true)
-  ⟹⟨(λ[ ξ·₂x ∶ 𝔹 ] not · value-λ (βλ·not · ` x)) value-true)· true
+  ⟹⟨ βλ· value-true ⟩
     not · (if true then falsenot else true)
-  ⟹⟨ ξ·₂ value-λ βif-true  ⟩
-    not · falsetrue)
   ⟹⟨ ξ·₂ value-λ (βλ· value-falsevalue-true) ⟩
     not · (if false then false else true then false else true)
   ⟹⟨ βif-falseξ·₂ value-λ βif-true  ⟩
+    not · false
-    true⟹⟨ βλ· value-false ⟩
+    if false then false else true
   ⟹⟨ βif-false ⟩
+    true
+  ∎
 
@@ -4327,915 +4332,990 @@ In general, we use typing _judgements_ of the form
     Γ ⊢ M ∶ A
 
 which asserts in type environment `Γ` that term `M` has type `A`.
-Here `Γ` provides types for all the free variables in `M`.
+Environment `Γ` provides types for all the free variables in `M`.
 
 Here are three examples. 
 
+* `` ∅ , f ∶ 𝔹 ⇒ 𝔹 , x ∶ 𝔹 ⊢ ` f · (` f · ` x) ∶  𝔹 ``
+* `` ∅ , f ∶ 𝔹 ⇒ 𝔹 ⊢ (λ[ x ∶ 𝔹 ] ` f · (` f · ` x)) ∶  𝔹 ⇒ 𝔹 ``
 * `` ∅ ⊢ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)) ∶  (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ``
 
-* `` ∅ , f ∶ 𝔹 ⇒ 𝔹 ⊢ (λ[ x ∶ 𝔹 ] ` f · (` f · ` x)) ∶  𝔹 ⇒ 𝔹 ``
-
-* `` ∅ , f ∶ 𝔹 ⇒ 𝔹 , x ∶ 𝔹 ⊢ ` f · (` f · ` x) ∶  𝔹 ``
-
-Environments are maps from free variables to types, built using `∅`
+Environments are partial maps from identifiers to types, built using `∅`
 for the empty map, and `Γ , x ∶ A` for the map that extends
 environment `Γ` by mapping variable `x` to type `A`.
 
+In an informal presentation of the formal semantics, 
+the rules for typing are written as follows.
+
+    Γ x ≡ A
+    ----------- Ax
+    Γ ⊢ ` x ∶ A
+
+    Γ , x ∶ A ⊢ N ∶ B
+    ------------------------ ⇒-I
+    Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
+
+    Γ ⊢ L ∶ A ⇒ B
+    Γ ⊢ M ∶ A
+    -------------- ⇒-E
+    Γ ⊢ L · M ∶ B
+
+    ------------- 𝔹-I₁
+    Γ ⊢ true ∶ 𝔹
+
+    -------------- 𝔹-I₂
+    Γ ⊢ false ∶ 𝔹
+
+    Γ ⊢ L : 𝔹
+    Γ ⊢ M ∶ A
+    Γ ⊢ N ∶ A
+    -------------------------- 𝔹-E
+    Γ ⊢ if L then M else N ∶ A
+
+As we will show later, the rules are deterministic, in that
+at most one rule applies to every term. 
+
+The proof rules come in pairs, with rules to introduce and to
+eliminate each connective, labeled `-I` and `-E`, respectively. As we
+read the rules from top to bottom, introduction and elimination rules
+do what they say on the tin: the first _introduces_ a formula for the
+connective, which appears in the conclusion but not in the premises;
+while the second _eliminates_ a formula for the connective, which appears in
+a premise but not in the conclusion. An introduction rule describes
+how to construct a value of the type (abstractions yield functions,
+true and false yield booleans), while an elimination rule describes
+how to deconstruct a value of the given type (applications use
+functions, conditionals use booleans).
+
+Here are the above rules formalised in Agda.
 
 
 
-Context : Set
 Context = PartialMap Type
 
 infix 10 _⊢_∶_
 
 data _⊢_∶_ : Context → Term → Type → Set where
   Ax : ∀ {Γ x A} →
     Γ x ≡ just A →
     Γ ⊢ ` x ∶ A
   ⇒-I : ∀ {Γ x N A B} →
     Γ , x ∶ A ⊢ N ∶ B →
     Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
   ⇒-E : ∀ {Γ L M A B} →
     Γ ⊢ L ∶ A ⇒ B →
     Γ ⊢ M ∶ A →
     Γ ⊢ L · M ∶ B
   𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ true ∶ 𝔹
   𝔹-I₂ : ∀ {Γ} →
     Γ ⊢ false ∶ 𝔹
   𝔹-E : ∀ {Γ L M N A} →
     Γ ⊢ L ∶ 𝔹 →
     Γ ⊢ M ∶ A →
     Γ ⊢ N ∶ A →
     Γ ⊢ if L then M else N ∶ A
 
 

 
-## Example type derivations
+#### Example type derivations
+
+Here are a couple of typing examples.  First, here is how
+they would be written in an informal description of the
+formal semantics.
+
+Derivation of `not`:
+
+    ------------ Ax    ------------- 𝔹-I₂    ------------- 𝔹-I₁
+    Γ₀ ⊢ ` x ∶ 𝔹       Γ₀ ⊢ false ∶ 𝔹         Γ₀ ⊢ true ∶ 𝔹
+    ------------------------------------------------------ 𝔹-E
+    Γ₀ ⊢ if ` x then false else true ∶ 𝔹
+    --------------------------------------------------- ⇒-I
+    ∅ ⊢ λ[ x ∶ 𝔹 ] if ` x then false else true ∶ 𝔹 ⇒ 𝔹
+
+where `Γ₀ = ∅ , x ∶ 𝔹`.
+
+Derivation of `two`:
+                            ----------------- Ax     ------------ Ax
+                            Γ₂ ⊢ ` f ∶ 𝔹 ⇒ 𝔹         Γ₂ ⊢ ` x ∶ 𝔹
+    ----------------- Ax    ------------------------------------- ⇒-E
+    Γ₂ ⊢ ` f ∶ 𝔹 ⇒ 𝔹        Γ₂ ⊢ ` f · ` x ∶ 𝔹
+    -------------------------------------------  ⇒-E
+    Γ₂ ⊢ ` f · (` f · ` x) ∶ 𝔹
+    ------------------------------------------ ⇒-I
+    Γ₁ ⊢ λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ∶ 𝔹 ⇒ 𝔹
+    ---------------------------------------------------------- ⇒-I
+    ∅ ⊢ λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ∶ 𝔹 ⇒ 𝔹
+
+where `Γ₁ = ∅ , f ∶ 𝔹 ⇒ 𝔹` and `Γ₂ = ∅ , f ∶ 𝔹 ⇒ 𝔹 , x ∶ 𝔹`.
+
+Here are the above derivations formalised in Agda.
 
 
 
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
 typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
 typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
 
 

 
+## Interaction with Agda
+
 Construction of a type derivation is best done interactively.
-We start with the declaration:
+Start with the declaration:
 
     typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
     typing₁ = ?
@@ -5269,4 +5349,275 @@ hole. After filling in all holes, the term is as above.
 
 The entire process can be automated using Agsy, invoked with C-c C-a.
 
+#### Non-examples
+
+We can also show that terms are _not_ typeable.
+For example, here is a formal proof that it is not possible
+to type the term `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ``.
+In other words, no type `A` is the type of this term.
+
+
+
+contradiction : ∀ {A B} → ¬ (𝔹 ≡ A ⇒ B)
+contradiction ()
+
+notyping : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
+notyping (⇒-I (⇒-I (⇒-E (Ax Γx) (Ax Γy)))) =  contradiction (just-injective Γx)
+
+

+
+#### Quiz
+
+For each of the following, given a type `A` for which it is derivable,
+or explain why there is no such `A`.
+
+1. `` ∅ , y ∶ A ⊢ λ[ x ∶ 𝔹 ] ` x ∶ 𝔹 ⇒ 𝔹 ``
+2. `` ∅ ⊢ λ[ y ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` y · ` x ∶ A ``
+3. `` ∅ ⊢ λ[ y ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` x · ` y ∶ A ``
+4. `` ∅ , x ∶ A ⊢ λ[ y : 𝔹 ⇒ 𝔹 ] `y · `x : A ``
+
+For each of the following, give type `A`, `B`, and `C` for which it is derivable,
+or explain why there are no such types.
+
+1. `` ∅ ⊢ λ[ y ∶ 𝔹 ⇒ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` y · ` x ∶ A ``
+2. `` ∅ , x ∶ A ⊢ x · x ∶ B ``
+3. `` ∅ , x ∶ A , y ∶ B ⊢ λ[ z ∶ C ] ` x · (` y · ` z) ∶ D ``
+
+
 
diff --git a/out/StlcProp.md b/out/StlcProp.md
index e5da2069..9085c13e 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -351,60 +351,73 @@ theorem.
       >update-permute); renamingjust≢nothing; (_,_↦_ to _,_∶_just-injective)
-openrenaming import Stlc
-import Data.Nat using (ℕ_,_↦_ to _,_∶_)
+open import Stlc
+import Data.Nat using (ℕ)
 
@@ -421,404 +434,404 @@ while for boolean types they are values `true` and `false`.
 
 
 
-data canonical_for_ : Term → Type → Set where
-  canonical-λ : ∀ {x A N B}: Term → canonicalType (λ[→ xSet ∶ A ] N) for (A ⇒ B)where
   canonical-truecanonical-λ : ∀ {x A N B} → canonical true(λ[ x ∶ A for] 𝔹N) for (A ⇒ B)
   canonical-falsecanonical-true : canonical false forcanonical true for 𝔹
-
-canonical-forms : ∀ {L A}canonical-false →: ∅ ⊢ L ∶ Acanonical →false Value Lfor →𝔹
+
+canonical-forms canonical: ∀ {L for A
-canonical-forms} (Ax→ ())∅ ()
-canonical-forms⊢ L ∶ A → Value L → canonical (⇒-IL ⊢N)for value-λ = canonical-λA
 canonical-forms (⇒-EAx ⊢L()) ⊢M) ()
 canonical-forms (⇒-I ⊢N) value-λ = canonical-λ
+canonical-forms (⇒-E ⊢L ⊢M) ()
+canonical-forms 𝔹-I₁ value-true = canonical-true
-canonical-forms 𝔹-I₂ value-false = canonical-false
 canonical-forms (𝔹-E𝔹-I₂ value-false = canonical-false
+canonical-forms (𝔹-E ⊢L ⊢M ⊢N) ()
 
@@ -832,191 +845,191 @@ step or it is a value.
 
 
 
-data Progress : Term → Set where
-  steps : ∀ {M N} → M ⟹ N → Progress M → Set where
   done  steps : ∀ {M} → Value {M N} → Progress M ⟹ N → Progress M
+  done  : ∀ {M} → Value M → Progress M
 
 progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1073,451 +1086,451 @@ This completes the proof.
 
 
 
-progress (Ax ())
-progress (⇒-I ⊢N) = done value-λ
-progress (⇒-E ⊢L ⊢M) with progress ⊢L())
 ...progress | steps L⟹L′ = steps (ξ·₁⇒-I ⊢N) = done value-λ
+progress (⇒-E ⊢L L⟹L′⊢M) with progress ⊢L
 ... | donesteps valueL with progressL⟹L′ ⊢M
-... | steps M⟹M′ = steps (ξ·₂ξ·₁ valueL M⟹M′L⟹L′)
 ... | done valueM with canonical-forms ⊢L valueL with progress ⊢M
 ... | steps M⟹M′ = steps (ξ·₂ valueL M⟹M′)
+... canonical-λ| =done valueM stepswith (βλ·canonical-forms valueM)⊢L valueL
 progress 𝔹-I₁ =... done value-true
-progress 𝔹-I₂ = done value-false
-progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
-... | stepscanonical-λ L⟹L′ = steps (βλ· valueM)
+progress 𝔹-I₁ = done value-true
+progress 𝔹-I₂ = done value-false
+progress steps (ξif𝔹-E ⊢L ⊢M L⟹L′⊢N)
-... | done valueL with canonical-formsprogress ⊢L valueL
 ... | steps L⟹L′ = steps (ξif L⟹L′)
+... canonical-true = steps βif-true
-... | done valueL with canonical-forms ⊢L canonical-falsevalueL
+... | canonical-true = steps βif-true
+... | canonical-false = steps βif-false
 
@@ -1538,68 +1551,68 @@ instead of induction on typing derivations.
 
 
 
-postulate
   progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1661,598 +1674,598 @@ Formally:
 
 
 
-data _∈_ : Id → Term → Set where
-  free-`  : ∀ {x} → x ∈ ` x
-  free-λ  : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N)where
   free-·₁ free-`  : ∀ {x} → x ∈ ` x
+  free-λ  : ∀ {x y A N} {→ y ≢ x L M} → x ∈ LN → x ∈ (Lλ[ ·y M)∶ A ] N)
   free-·₂ : ∀ {xfree-·₁ L: M}∀ →{x xL ∈ M} → x ∈ (L → ·x ∈ (L · M)
   free-if₁free-·₂ : ∀ {x L M N} → x L M} ∈→ Lx →∈ xM ∈→ (ifx ∈ (L then· M else N)
   free-if₂free-if₁ : ∀ {x L :M ∀N} {x→ Lx M∈ N}L → x ∈ M → x ∈ (if L then M L then M else N)
   free-if₃free-if₂ : ∀ {x L :M ∀N} {x→ Lx M∈ N}M → x ∈ N → x ∈ (if L then M L then M else N)
+  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
 
@@ -2262,131 +2275,131 @@ A term in which no variables appear free is said to be _closed_.
 
 
 
-_∉_ : Id → Term → Set
-x ∉ M = ¬ (x ∈ M)
-
-closed : Term →: Id → Term → Set
 closed M = ∀ {x} → x ∉ M = ¬ (x ∈ M)
+
+closed : Term → Set
+closed M = ∀ {x} → x ∉ M
 
@@ -2396,240 +2409,240 @@ Here are proofs corresponding to the first two examples above.
 
 
 
-f≢x : f ≢ x
 f≢x ()
 
 example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
-example-free₁ = free-λ f≢x (free-·₂ free-`)
-
-example-free₂ : x ∈ (λ[ f ∉∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₁ (λ[= ffree-λ ∶ (𝔹 ⇒f≢x 𝔹) ] ` f(free-·₂ · ` xfree-`)
+
 example-free₂ (free-λ: f ∉ f≢f(λ[ _)f =∶ f≢f(𝔹 ⇒ 𝔹) ] ` f · ` x)
+example-free₂ (free-λ f≢f _) = f≢f refl
 
@@ -2641,367 +2654,367 @@ Prove formally the remaining examples given above.
 
 
 
-postulate
   example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
-  example-free₄ : f ∈ ((λ[ f ∶ (𝔹] ⇒` 𝔹)f · ]` ` f · ` x) · ` f)
   example-free₅example-free₄ : xf ∉∈ (((λ[ f ∶ (𝔹 f⇒ ∶ (𝔹) ] ⇒` 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x) · ` f)
   example-free₆example-free₅ : fx ∉ (λ[ f ∶ (𝔹 (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · ` x)
+  example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
 
@@ -3020,115 +3033,115 @@ then `Γ` must assign a type to `x`.
 
 
 
-free-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
 
@@ -3164,454 +3177,454 @@ _Proof_: We show, by induction on the proof that `x` appears
 
 
 
-free-lemma free-` (Ax Γx≡A) = (_ , Γx≡A)
 free-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = free-lemma x∈L ⊢L
-free-lemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = free-lemma x∈Mx∈L ⊢M⊢L
 free-lemma (free-if₁free-·₂ x∈Lx∈M) (𝔹-E⇒-E ⊢L ⊢M) ⊢L ⊢M ⊢N) = free-lemma x∈Lx∈M ⊢L⊢M
 free-lemma (free-if₁ x∈L) (free-if₂𝔹-E x∈M)⊢L (𝔹-E⊢M ⊢N) ⊢L ⊢M ⊢N) = free-lemma x∈Mx∈L ⊢M⊢L
 free-lemma (free-if₂ x∈M) (free-if₃𝔹-E x∈N)⊢L (𝔹-E⊢M ⊢N) ⊢L ⊢M ⊢N) = free-lemma x∈Nx∈M ⊢N⊢M
 free-lemma (free-if₃ x∈N) (free-λ𝔹-E {x}⊢L {y}⊢M y≢x⊢N) x∈N)= (⇒-I ⊢N) with free-lemma x∈N ⊢N
 ...free-lemma (free-λ {x|} Γx≡C with {y} ≟y≢x x
-...x∈N) (⇒-I ⊢N|) yeswith y≡xfree-lemma =x∈N ⊥-elim (y≢x y≡x)⊢N
 ... | no  _Γx≡C with   = y ≟ x
+... | yes y≡x = ⊥-elim (y≢x y≡x)
+... | no  _   = Γx≡C
 
@@ -3629,68 +3642,68 @@ typed in the empty context is closed (has no free variables).
 
 
 
-postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
 
@@ -3699,294 +3712,179 @@ typed in the empty context is closed (has no free variables).