From 8fb67556ed9852fe8503683c4d32f7122dad8fc5 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Wed, 19 Jul 2017 13:02:23 +0100 Subject: [PATCH] last fixes to Stlc and StlcProp before sending out for comment --- index.md | 4 + out/Basics.md | 30 +- out/Stlc.md | 6793 +++++++++++++++--------------- out/StlcProp.md | 9871 ++++++++++++++++++++++---------------------- src/Basics.lagda | 26 +- src/Stlc.lagda | 25 +- src/StlcProp.lagda | 33 +- 7 files changed, 8458 insertions(+), 8324 deletions(-) diff --git a/index.md b/index.md index 13e9d65a..28d9da5c 100644 --- a/index.md +++ b/index.md @@ -3,7 +3,11 @@ title : Table of Contents layout : page --- + + - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }}) - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }}) - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }}) + diff --git a/out/Basics.md b/out/Basics.md index 688d29e3..d0202f22 100644 --- a/out/Basics.md +++ b/out/Basics.md @@ -50,16 +50,16 @@ proofs and sound informal reasoning about program behavior. The other sense in which functional programming is "functional" is that it emphasizes the use of functions (or methods) as -*first-class* values -- i.e., values that can be passed as +_first-class_ values -- i.e., values that can be passed as arguments to other functions, returned as results, included in data structures, etc. The recognition that functions can be treated as data in this way enables a host of useful and powerful idioms. -Other common features of functional languages include *algebraic -data types* and *pattern matching*, which make it easy to +Other common features of functional languages include _algebraic +data types_ and _pattern matching_, which make it easy to construct and manipulate rich data structures, and sophisticated -*polymorphic type systems* supporting abstraction and code reuse. +_polymorphic type systems_ supporting abstraction and code reuse. Agda shares all of these features. This chapter introduces the most essential elements of Agda. @@ -67,7 +67,7 @@ This chapter introduces the most essential elements of Agda. ## Enumerated Types One unusual aspect of Agda is that its set of built-in -features is *extremely* small. For example, instead of providing +features is _extremely_ small. For example, instead of providing the usual palette of atomic data types (booleans, integers, strings, etc.), Agda offers a powerful mechanism for defining new data types from scratch, from which all these familiar types arise @@ -87,7 +87,7 @@ very simple example. ### Days of the Week The following declaration tells Agda that we are defining -a new set of data values -- a *type*. +a new set of data values -- a _type_. 
 
@@ -358,7 +358,7 @@ One thing to note is that the argument and return types of
 this function are explicitly declared.  Like most functional
 programming languages, Agda can often figure out these types for
 itself when they are not given explicitly -- i.e., it performs
-*type inference* -- but we'll include them to make reading
+_type inference_ -- but we'll include them to make reading
 easier.
 
 Having defined a function, we should check that it works on
@@ -372,13 +372,13 @@ would be an excellent moment to fire up Agda and try this for yourself.
 Load this file, `Basics.lagda`, load it using `C-c C-l`, submit the
 above example to Agda, and observe the result.
 
-Second, we can record what we *expect* the result to be in the
+Second, we can record what we _expect_ the result to be in the
 form of an Agda type:
 
 
 
-test_nextWeekdaytest-nextWeekday 
 
-test_nextWeekdaytest-nextWeekday 
 
 There is no essential difference between the definition for
-`test_nextWeekday` here and the definition for `nextWeekday` above,
+`test-nextWeekday` here and the definition for `nextWeekday` above,
 except for the new symbol for equality `≡` and the constructor `refl`.
 The details of these are not important for now (we'll come back to them in
 a bit), but essentially `refl` can be read as "The assertion we've made
 can be proved by observing that both sides of the equality evaluate to the
 same thing, after some simplification."
 
-Third, we can ask Agda to *compile* some program involving our definition,
+Third, we can ask Agda to _compile_ some program involving our definition,
 This facility is very interesting, since it gives us a way to construct
-*fully certified* programs. We'll come back to this topic in later chapters.
+_fully certified_ programs. We'll come back to this topic in later chapters.
diff --git a/out/Stlc.md b/out/Stlc.md
index d2b6f035..8a30e9c6 100644
--- a/out/Stlc.md
+++ b/out/Stlc.md
@@ -20,6 +20,7 @@ and the next chapter reviews its main properties (progress and preservation).
 The new technical challenges arise from the mechanisms of
 _variable binding_ and _substitution_.
 
+
 
 We choose booleans as our base type for simplicity.  At the end of the
 chapter we'll see how to add numbers as a base type, and in later
@@ -38,244 +40,244 @@ lists, records, subtyping, and mutable state.
 
 
 
-open import Maps using (Id; id; _≟_(Id; PartialMapid; module_≟_; PartialMap; module PartialMap)
 open PartialMap using (∅; just-injective) renaming renaming (_,_↦_ to _,_↦_ to _,_∶_)
 open import Data.Nat usingData.Nat (ℕ)
-openusing import Data.Maybe using (Maybe; just; nothingℕ)
 open import Relation.NullaryData.Maybe using (DecMaybe; just; nothing)
+open import Relation.Nullary using yes; no(Dec; ¬_)
-openyes; no; ¬_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_(_≡_; _≢_; refl)
 
@@ -301,79 +303,79 @@ And here it is formalised in Agda.
 
 
 
-infixr 20 _⇒_
 
 data Type : Set where
   _⇒_ : Type → Type: →Type → Type
-  𝔹 → :Type
+  𝔹 : Type
 
@@ -409,213 +411,213 @@ And here it is formalised in Agda.
 
 
 
-infixl 20 _·_
 infix  15 λ[_∶_]_
 infix  15 if_then_else_
 
 data Term : Set where
-  ` : Id → Term
   λ[_∶_]_` : Id → TypeTerm
+  λ[_∶_]_ →: Id Term → Type → Term → Term
   _·_ : Term → Term: →Term Term
-  true : Term
-  false : Term
-  if_then_else_ : Term → Term → Term
+  true : Term
+  false : Term
+  if_then_else_ Term: →Term Term → Term → Term → Term
 
@@ -670,246 +672,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 ` x then ` x then false else true)
 two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x⇒ ∶𝔹 𝔹] λ[ x ∶ 𝔹 ] ` f · (` f` ·f `· (` f · ` x)
 
@@ -984,369 +986,369 @@ to be weaker than application. For instance,
 
 
 
-ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹) ≡⇒ (𝔹 ⇒ 𝔹) ⇒≡ (𝔹 ⇒ 𝔹)
-ex₁ ⇒ (𝔹 =⇒ 𝔹)
+ex₁ = refl
 
 ex₂ : two · not · true ≡ (two · true not)≡ ·(two true
-ex₂· not) · =true
+ex₂ = refl
 
 ex₃ : λ[ f ∶ 𝔹: ⇒ 𝔹 ] λ[ f ∶ 𝔹 x⇒ ∶𝔹 𝔹] λ[ x ∶ 𝔹 ] ` f · (` f` ·f `· x)(` f · ` x)
       ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f∶ ·𝔹 (`] f(` ·f `· (` f · ` x))))
 ex₃ = refl
 
@@ -1398,130 +1400,130 @@ The predicate `Value M` holds if term `M` is a value.
 
 
 
-data Value : Term → Set where
-  value-λ     : ∀Term {x A N} → ValueSet (λ[where
+  value-λ     : ∀ {x ∶ A ] N)} → Value (λ[ x ∶ A ] N)
   value-true  : Value  : Value true
   value-false : Value false
 
@@ -1594,646 +1596,646 @@ Here is the formal definition in Agda.
 
 
 
-_[_:=_] : Term → Id: → Term → Id → Term → Term
 (` x′) [ x := V ][ withx := xV ≟] x′
-...with x |≟ yes _ = V
-... | no  _ = ` x′
 ... | yes _ = V
+... | no  (λ[_ = ` x′ ∶
+(λ[ A′x′ ] N′)∶ [A′ x] := VN′) ][ withx := xV ≟] x′
-...with x |≟ yes _ = λ[ x′ ∶ A′ ] N′
 ... | yes _ = λ[ x′ ∶ A′ |] no  _ = λ[ x′ ∶ A′ ] (N′
+... | no  _ = λ[ x′ ∶ [A′ x] := V(N′ ])
-(L′[ x := ·V M′])
+(L′ [· x := VM′) ][ =x  (L′ := V [] x= := V  (L′ ])[ ·x (M′:= V []) x· := V(M′ [ x := V ])
 (true) [ x := V ][ =x true:= V ] = true
 (false) [ x := V ][ =x := V ] = false
 (if L′ then M′ else N′) [else x := VN′) ][ =x
-  if := V (L′] =
+  if [ x := V(L′ [ x := V ]) then (M′ [then x := V(M′ [ x := V ]) else (N′ [else x := V(N′ [ x := V ])
 
@@ -2265,666 +2267,666 @@ Here is confirmation that the examples above are correct.
 
 
 
-ex₁₁ : ` f [ f := notf [ ]f ≡  := not ] ≡  not
 ex₁₁ = refl
 
 ex₁₂ : true [ f: :=true not[ ]f ≡:= truenot ] ≡ true
 ex₁₂ = refl
 
 ex₁₃ : (` f · true): [(` f :=· nottrue) [ ]f ≡:= not ] ≡ not · true
 ex₁₃ = refl
 
 ex₁₄ : (` f · (`: f(` ·f true))· (` f [· ftrue)) := not[ ]f := not ] ≡ not · (not · · (not · true)
 ex₁₄ = refl
 
 ex₁₅ : (λ[ x ∶ 𝔹 ] ` f · (` f` ·f `· x))(` [ f :=· not` x)) [ ]f ≡:= λ[ xnot ∶] 𝔹≡ λ[ x ∶ 𝔹 ] not · (not · `· (not · ` x)
 ex₁₅ = refl
 
 ex₁₆ : (λ[ y ∶ 𝔹 ] ` y) [𝔹 x] ` y) [ x := true ] ≡ λ[ ytrue ∶] 𝔹≡ ]λ[ ` y
-ex₁₆ ∶ 𝔹 ] =` y
+ex₁₆ = refl
 
 ex₁₇ : (λ[ x ∶ 𝔹 ] ` x) [𝔹 x] ` x) [ x := true ] ≡ λ[ xtrue ∶] 𝔹≡ ]λ[ ` x
-ex₁₇ ∶ 𝔹 ] =` x
+ex₁₇ = refl
 
@@ -2998,569 +3000,569 @@ Here are the above rules formalised in Agda.
 
 
 
-infix 10 _⟹_ 
 
 data _⟹_ : Term → Term: →Term Set→ Term → Set where
   ξ·₁ : ∀ {L L′ M}∀ →
-    {L ⟹ L′ →
-    L · M} →
+    L ⟹ L′ →
+    L · M ⟹ L′ · M
   ξ·₂ : ∀ {V M M′: }∀ {V M M′} →
     Value V →
     M ⟹ M′ →
     V · M ⟹ V · M′
-  βλ· ⟹ V · : ∀ {x AM′
+  βλ· N: V}∀ →{x ValueA N V} → Value V →
     (λ[ x ∶ A ] N) ·∶ VA ⟹] N) [· xV :=⟹ VN ][ x := V ]
   ξif : ∀ {L L′ M N}{L L′ M N} →
     L ⟹ L′ →    
     if L then M elseL Nthen ⟹M if L′ then M else N ⟹ if L′ then M else N
   βif-true : ∀ {M N} →
-    if true then M else N ⟹ M
-  βif-false : ∀ {M N} →
     if true then M else N ⟹ M
+  βif-false : ∀ {M N} →
+    if false then M else N ⟹M else N ⟹ N
 
@@ -3630,189 +3632,189 @@ Here it is formalised in Agda.
 
 
 
-infix 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_ 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : Term → Term: →Term Set→ Term → Set where
   _∎ : ∀ M → M ⟹* M → M ⟹* M
   _⟹⟨_⟩_ : ∀ L {M N}: →∀ L ⟹{M MN} → ML ⟹*⟹ NM → LM ⟹* N → L ⟹* N
 
@@ -3832,477 +3834,477 @@ out example reductions in an appealing way.
 
 
 
-reduction₁ : not · true ⟹* false ⟹* false
 reduction₁ =
     not · true
   ⟹⟨ βλ· value-true ⟩
-    if true then false else true
-  ⟹⟨ βif-true ⟩
     if true then false else true
   ⟹⟨ βif-true ⟩
+    false
+  ∎
 
 reduction₂ : two · not · true ⟹* true
 reduction₂ =
     two · not · true
   ⟹⟨ ξ·₁ (βλ· value-λ)ξ·₁ (βλ· value-λ) ⟩
     (λ[ x ∶ 𝔹 ] not · (not · `· x))(not · ` x)) · true
   ⟹⟨ βλ· value-true ⟩
     not · (not · · (not · true)
   ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
     not · (if true then false else true)
-  ⟹⟨ ξ·₂ value-λ βif-true  ⟩
-    not · false
-  ⟹⟨ βλ· value-false ⟩
-    (if true then false else true)
+  ⟹⟨ ξ·₂ value-λ βif-true  ⟩
+    not · false
+  ⟹⟨ βλ· value-false false then false else true
-  ⟹⟨ βif-false ⟩
     if false then false else true
   ⟹⟨ βif-false ⟩
+    true
+  ∎
 
@@ -4391,683 +4393,683 @@ Here are the above rules formalised in Agda.
 
 
 
-Context : Set
 Context = PartialMap Type
 
 infix 10 _⊢_∶_ 10 _⊢_∶_
 
 data _⊢_∶_ : Context → Term → Type → Term Set→ Type → Set where
   Ax : ∀ {Γ x A}: ∀ {Γ x A} →
     Γ x ≡ just Ax →≡ just A →
     Γ ⊢ ` x ∶ A
   ⇒-I : ∀ {Γ x N: A∀ B}{Γ →x
-    Γ , x ∶ A ⊢ N ∶A B} →
     Γ ⊢, λ[ x ∶ A ⊢ N ∶ B →
+    Γ A⊢ ]λ[ Nx ∶ A ] N ∶ A ⇒ B
   ⇒-E : ∀ {Γ L M: A∀ B}{Γ →L M A B} →
     Γ ⊢ L ∶ A ⇒ B →
     Γ ⊢ M ∶ A →
     Γ ⊢ L · M ∶ B
-  𝔹-I₁ :B
+  𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ true ∶ 𝔹⊢
-  𝔹-I₂ true ∶ : ∀ {Γ} →
-    Γ ⊢ false ∶ 𝔹
   𝔹-E𝔹-I₂ : ∀ {Γ} L→
+    Γ ⊢ false ∶ 𝔹
+  𝔹-E M: N∀ A}{Γ →L
-    Γ ⊢ L ∶ 𝔹 →
-    Γ ⊢ M ∶ A →
-    Γ ⊢ N ∶ A} →
     Γ ⊢ if L then∶ 𝔹 →
+    Γ ⊢ M ∶ A →
+    Γ ⊢ N ∶ A →
+    Γ ⊢ if elseL Nthen ∶M else N ∶ A
 
@@ -5109,205 +5111,205 @@ Here are the above derivations formalised in Agda.
 
 
 
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
 typing₁ = ⇒-I (𝔹-E (Ax⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒two 𝔹)∶ ⇒ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
 typing₂ = ⇒-I (⇒-I (⇒-E⇒-I (Ax⇒-I refl) (⇒-E (Ax refl) refl) (Ax⇒-E (Ax refl) (Ax refl))))
 
@@ -5352,257 +5354,338 @@ 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.
+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 `` true ·
+false ``.  In other words, no type `A` is the type of this term.  It
+cannot be typed, because doing so requires that the first term in the
+application is both a boolean and a function.
 
 
 
-contradictionnotyping₂ : ∀ {A B} → ¬ (𝔹 ≡ A ⇒ B)
-contradiction ()
-
-notyping : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
-notyping (⇒-I→ (⇒-I¬ (⇒-E∅ (Ax⊢ Γxtrue · false ∶ A) (Ax
+notyping₂ Γy)))) =  contradiction (just-injective⇒-E () _)
+
+

+
+As a second example, here is a formal proof that it is not possible to
+type `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y `` It cannot be typed, because
+doing so requires `x` to be both boolean and a function.
+
+
+
+contradiction : ∀ {A B} → ¬ (𝔹 ≡ A ⇒ B)
+contradiction ()
+
+notyping₁ : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
+notyping₁ (⇒-I (⇒-I (⇒-E (Ax Γx) _))) =  contradiction (just-injective Γx)
 
 

 
+
 #### Quiz
 
 For each of the following, given a type `A` for which it is derivable,
diff --git a/out/StlcProp.md b/out/StlcProp.md
index 9085c13e..bdc63141 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -426,412 +426,415 @@ theorem.
 
 ## Canonical Forms
 
+
+
+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 function types the canonical forms are lambda-abstractions,
 while for boolean types they are values `true` and `false`.  
 
 
 
-data canonical_for_ : Term → Type → Set where Set where
   canonical-λ : ∀ {x A N B}∀ →{x canonicalA N B} → (λ[ x ∶ Acanonical ] N) for (λ[ x ∶ A ] ⇒ BN) for (A ⇒ B)
   canonical-true : canonical canonical true for 𝔹
   canonical-false : canonical false forcanonical false for 𝔹
 
 canonical-forms : ∀ {L A} →: ∅∀ ⊢ {L ∶A} A→ →∅ Value⊢ L ∶ LA → canonicalValue L → canonical L for A
 canonical-forms (Ax ()) ()
 canonical-forms (⇒-I ⊢N) value-λ =) value-λ = canonical-λ
 canonical-forms (⇒-E ⊢L ⊢M) ()
-canonical-forms 𝔹-I₁ value-true = canonical-true
-canonical-forms 𝔹-I₂ value-false = canonical-false
-canonical-forms (𝔹-E⇒-E ⊢L ⊢M ⊢N) ()
+canonical-forms 𝔹-I₁ value-true = canonical-true
+canonical-forms 𝔹-I₂ value-false = canonical-false
+canonical-forms (𝔹-E ⊢L ⊢M ⊢N) ()
 
@@ -845,201 +848,202 @@ step or it is a value.
 
 
 
-data Progress : Term → Set where Set where
   steps : ∀ {M N} →: M∀ ⟹{M N →} Progress→ M ⟹ N → Progress M
   done  : ∀ {M} → Value M → ProgressValue M → Progress M
 
 progress : ∀ {M A} →: ∅∀ ⊢ {M ∶A} A→ →∅ Progress⊢ M ∶ A → Progress M
 
 

 
-The proof is a relatively
-straightforward extension of the progress proof we saw in
+
+
+We give the proof in English first, then the formal version.
 
 _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
 
@@ -1086,451 +1090,451 @@ This completes the proof.
 
 
 
-progress (Ax ())
-progress (⇒-I ⊢N) =()) done value-λ
 progress (⇒-E⇒-I ⊢L ⊢M⊢N) with= progressdone ⊢Lvalue-λ
 ...progress |(⇒-E steps⊢L L⟹L′⊢M) with progress =⊢L
+... | steps (ξ·₁ L⟹L′)
-... |= done valueL with progress ⊢M
-... | steps M⟹M′(ξ·₁ L⟹L′)
+... | done valueL with progress =⊢M
+... | steps (ξ·₂ valueLM⟹M′ M⟹M′)
-... | done valueM with canonical-forms ⊢L valueL
-... | canonical-λ = steps (ξ·₂ valueL M⟹M′)
+... | done valueM with canonical-forms ⊢L valueL
+... | (βλ·canonical-λ valueM)
-progress 𝔹-I₁ = donesteps value-true(βλ· valueM)
 progress 𝔹-I₁ = done 𝔹-I₂ = done value-falsevalue-true
 progress (𝔹-E𝔹-I₂ ⊢L= ⊢Mdone value-false ⊢N) with
+progress progress(𝔹-E ⊢L
-... |⊢M steps⊢N) L⟹L′with progress = steps (ξif L⟹L′)
-... | done valueL with canonical-forms ⊢L valueL
 ... | canonical-true = steps βif-trueL⟹L′ = steps (ξif L⟹L′)
 ... | canonical-falsedone valueL with canonical-forms ⊢L valueL
+... | canonical-true = steps βif-true
+... steps| canonical-false = steps βif-false
 
@@ -1551,68 +1555,68 @@ instead of induction on typing derivations.
 
 
 
-postulate
   progress′ : ∀ M {A} → ∅ ⊢ M ∶ A: →∀ ProgressM {A} → ∅ ⊢ M ∶ A → Progress M
 
@@ -1627,9 +1631,12 @@ substitution.  Working from top to bottom (from the high-level
 property we are actually interested in to the lowest-level
 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
+  
+
+  - The one case that is significantly different is the one for the
     `βλ·` 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 ... 
@@ -1674,598 +1681,598 @@ Formally:
 
 
 
-data _∈_ : Id → Term → Set where
-  free-`  : ∀_∈_ {x}: Id → x ∈ ` xTerm → Set where
   free-λ  : ∀ {x y Afree-` N  }: →∀ y ≢{x} x→ →x x∈ ∈` N → x ∈ (λ[ y
+  free-λ  : ∶∀ A ] N)
-  free-·₁ : ∀ {x y A N} → y ≢ x → x ∈ LN M} → x ∈ L → x ∈ (Lλ[ ·y M∶ A ] N)
   free-·₂free-·₁ : ∀ : ∀ {x L M} → x →∈ xL ∈→ Mx →∈ x ∈ (L · M)
   free-if₁free-·₂ : ∀ {x ∀L {xM} L→ Mx N} → x ∈ LM → x ∈ (L x· ∈ (if L then M else N)
   free-if₂free-if₁ : ∀ {x L M N} → x ∈ :L ∀→ {x ∈ (if L M N} →then x ∈ M → xelse ∈ (if L then M else N)
   free-if₃free-if₂ : ∀ {x L M N} → x ∈ :M ∀→ {x ∈ (if L M N} →then xM ∈ N → xelse ∈ (if L then M else N)
+  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
 
@@ -2275,131 +2282,131 @@ A term in which no variables appear free is said to be _closed_.
 
 
 
-_∉_ : Id → Term → Set
 x ∉ M = ¬ (x ∈ M)
-
-closed : Term → Set
-closed M= =¬ ∀ {(x} ∈ M→)
+
+closed : Term → Set
+closed M = ∀ {x} → x ∉ M
 
@@ -2409,240 +2416,240 @@ Here are proofs corresponding to the first two examples above.
 
 
 
-f≢x : f ≢ x
-f≢x ()
-
-example-free₁ : x ∈ (λ[ f: ∶f (𝔹≢ ⇒ 𝔹) ] ` f · ` x)
 example-free₁ = free-λ f≢x (free-·₂ free-`)()
 
 example-free₂example-free₁ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
 example-free₂example-free₁ (= free-λ f≢x (free-·₂ free-`)
+
+example-free₂ : f ∉ (λ[ f ∶ (𝔹 f≢f⇒ _)𝔹) ] =` f≢ff · ` x)
+example-free₂ (free-λ f≢f _) = f≢f refl
 
@@ -2654,367 +2661,367 @@ Prove formally the remaining examples given above.
 
 
 
-postulate
   example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
-  example-free₄ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ∈] ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
+  example-free₄ f)
-  example-free₅ : xf ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ∉] (λ[` f f· ∶` (𝔹x) ⇒· 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
   example-free₆example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) :] f ∉ (λ[ fx ∶ (𝔹 ] ` f ⇒· 𝔹` x) ]
+  example-free₆ λ[: x ∶ 𝔹 ] ` f ·∉ `(λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
 
@@ -3033,115 +3040,115 @@ then `Γ` must assign a type to `x`.
 
 
 
-free-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B: →∀ Γ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
 
@@ -3177,454 +3184,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Γx≡A)
 free-lemma (free-·₂free-·₁ x∈L) (⇒-E ⊢L ⊢M) x∈M)= (⇒-E ⊢Lfree-lemma ⊢M)x∈L = free-lemma x∈M ⊢M⊢L
 free-lemma (free-if₁free-·₂ x∈Lx∈M) (𝔹-E⇒-E ⊢L ⊢M) = free-lemma x∈M ⊢N) = free-lemma x∈L ⊢L⊢M
 free-lemma (free-if₂free-if₁ x∈Mx∈L) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈L ⊢N) = free-lemma x∈M ⊢M⊢L
 free-lemma (free-if₃free-if₂ x∈Nx∈M) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈M ⊢N) = ⊢M
+free-lemma x∈N ⊢N(free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈N ⊢N
 free-lemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with free-lemma x∈N ⊢N
-... | Γx≡C with y ≟ x free-lemma x∈N ⊢N
 ... | Γx≡C with y ≟ x
+... | yes y≡x = ⊥-elim (y≢x y≡x)
 ... | no  _   = Γx≡C
 
@@ -3642,68 +3649,68 @@ typed in the empty context is closed (has no free variables).
 
 
 
-postulate
   ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
 
@@ -3712,179 +3719,179 @@ typed in the empty context is closed (has no free variables).