revising Stlc and StlcProp

src/Maps.lagda

@@ -36,7 +36,6 @@ standard library, wherever they overlap.
 open import Data.Nat         using (ℕ)
 open import Data.Empty       using (⊥; ⊥-elim)
 open import Data.Maybe       using (Maybe; just; nothing)
--- open import Data.String      using (String)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
                              using (_≡_; refl; _≢_; trans; sym)
@@ -54,7 +53,7 @@ we repeat its definition here.
 
 \begin{code}
 data Id : Set where
-  id : ℕ → Id   {- String → Id -}
+  id : ℕ → Id
 \end{code}
 
 We recall a standard fact of logic.
@@ -69,7 +68,7 @@ by deciding equality on the underlying strings.
 
 \begin{code}
 _≟_ : (x y : Id) → Dec (x ≡ y)
-id x ≟ id y with x Data.Nat.≟ y {- x Data.String.≟ y -}
+id x ≟ id y with x Data.Nat.≟ y
 id x ≟ id y | yes refl  =  yes refl
 id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
   where
@@ -77,15 +76,6 @@ id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
     id-inj refl  =  refl
 \end{code}
 
-We define some identifiers for future use.
-
-\begin{code}
-x y z : Id
-x = id 0  -- id "x"
-y = id 1  -- id "y"
-z = id 2  -- id "z"
-\end{code}
-
 ## Total Maps
 
 Our main job in this chapter will be to build a definition of
@@ -135,8 +125,8 @@ takes `x` to `v` and takes every other key to whatever `ρ` does.
 
   _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A
   (ρ , x ↦ v) y with x ≟ y
-  ... | yes x=y = v
-  ... | no  x≠y = ρ y
+  ... | yes x≡y = v
+  ... | no  x≢y = ρ y
 \end{code}
 
 This definition is a nice example of higher-order programming.
@@ -147,25 +137,30 @@ 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:
 
 \begin{code}
-  ρ₀ : TotalMap ℕ
-  ρ₀ = always 0 , x ↦ 42 , y ↦ 69
+  module example where
+
+    x y z : Id
+    x = id 0
+    y = id 1
+    z = id 2
+
+    ρ₀ : TotalMap ℕ
+    ρ₀ = always 0 , x ↦ 42 , y ↦ 69
+
+    test₁ : ρ₀ x ≡ 42
+    test₁ = refl
+
+    test₂ : ρ₀ y ≡ 69
+    test₂ = refl
+
+    test₃ : ρ₀ z ≡ 0
+    test₃ = refl
 \end{code}
 
 This completes the definition of total maps.  Note that we don't
 need to define a `find` operation because it is just function
 application!
 
-\begin{code}
-  test₁ : ρ₀ x ≡ 42
-  test₁ = refl
-
-  test₂ : ρ₀ y ≡ 69
-  test₂ = refl
-
-  test₃ : ρ₀ z ≡ 0
-  test₃ = refl
-\end{code}
-
 To use maps in later chapters, we'll need several fundamental
 facts about how they behave.  Even if you don't work the following
 exercises, make sure you understand the statements of

src/Stlc.lagda

@@ -7,10 +7,10 @@ permalink : /Stlc
 This chapter defines the simply-typed lambda calculus.
 
 ## Imports
+
 \begin{code}
 open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
 open PartialMap using (∅) renaming (_,_↦_ to _,_∶_)
--- open import Data.String using (String)
 open import Data.Nat using (ℕ)
 open import Data.Maybe using (Maybe; just; nothing)
 open import Relation.Nullary using (Dec; yes; no)
@@ -45,8 +45,8 @@ data Term : Set where
 Example terms.
 \begin{code}
 f x : Id
-f  =  id 0 -- id "f"
-x  =  id 1 -- id "x"
+f  =  id 0
+x  =  id 1
 
 not two : Term 
 not =  λ[ x ∶ 𝔹 ] (if var x then false else true)
@@ -104,26 +104,6 @@ data _⟹_ : Term → Term → Set where
 
 ## Reflexive and transitive closure
 
-\begin{code}
-{-
-Rel : Set → Set₁
-Rel A = A → A → Set
-
-infixl 10 _>>_
-
-data _* {A : Set} (R : Rel A) : Rel A where
-  ⟨⟩ : ∀ {x : A} → (R *) x x
-  ⟨_⟩ : ∀ {x y : A} → R x y → (R *) x y
-  _>>_ : ∀ {x y z : A} → (R *) x y → (R *) y z → (R *) x z
-
-infix 10 _⟹*_
-
-_⟹*_ : Rel Term
-_⟹*_ = (_⟹_) *
--}
-\end{code}
-
-## Notation for setting out reductions
 
 \begin{code}
 infix 10 _⟹*_ 
@@ -164,50 +144,6 @@ reduction₂ =
 Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
-\begin{code}
-{-
-infixr 2 _⟹⟨_⟩_
-infix  3 _∎
-
-_⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N
-L ⟹⟨ L⟹M ⟩ M⟹*N  =  ⟨ L⟹M ⟩ >> M⟹*N
-
-_∎ : ∀ M → M ⟹* M
-M ∎  =  ⟨⟩
--}
-\end{code}
-
-## Example reduction derivations
-
-\begin{code}
-{-
-reduction₁ : not · true ⟹* false
-reduction₁ =
-    not · true
-  ⟹⟨ β⇒ value-true ⟩
-    if true then false else true
-  ⟹⟨ β𝔹₁  ⟩
-    false
-  ∎
-
-reduction₂ : two · not · true ⟹* true
-reduction₂ =
-    two · not · true
-  ⟹⟨ γ⇒₁ (β⇒ value-λ) ⟩
-    (λ[ x ∶ 𝔹 ] not · (not · var x)) · true
-  ⟹⟨ β⇒ value-true ⟩
-    not · (not · true)
-  ⟹⟨ γ⇒₂ value-λ (β⇒ value-true) ⟩
-    not · (if true then false else true)
-  ⟹⟨ γ⇒₂ value-λ β𝔹₁ ⟩
-    not · false
-  ⟹⟨ β⇒ value-false ⟩
-    if false then false else true
-  ⟹⟨ β𝔹₂ ⟩
-    true
-  ∎
--}
-\end{code}
 
 ## Type rules
 
@@ -255,20 +191,19 @@ We start with the declaration:
     typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
     typing₁ = ?
 
-Typing C-L (control L) causes Agda to create a hole and tell us its
-expected type.
+Typing C-l causes Agda to create a hole and tell us its expected type.
 
     typing₁ = { }0
     ?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
 
-Now we fill in the hole by typing C-R (control R). Agda observes that
+Now we fill in the hole by typing C-c C-r. Agda observes that
 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 ∶ 𝔹
 
-Again we fill in the hole by typing C-R. Agda observes that the
+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.
 
@@ -277,7 +212,7 @@ outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
     ?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹
     ?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹
 
-Again we fill in the three holes by typing C-R in each. Agda observes
+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
 `𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
 that `(∅ , x ∶ 𝔹) x = just 𝔹`, which can in turn be specified with a

src/StlcProp.lagda

@@ -193,16 +193,16 @@ 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.
 For example:
 
-  - `x` appears free, but `f` does not, in `λ[ f ∶ (A ⇒ B) ] f · x`
-  - both `f` and `x` appear free in `(λ[ f ∶ (A ⇒ B) ] f · x) · f`;
+  - `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 ∶ (A ⇒ B) ] (λ[ x ∶ A ] f · x)`
+  - no variables appear free in `λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x`
 
 Formally:
 
 \begin{code}
 data _∈_ : Id → Term → Set where
-  free-var  : ∀ {x} → x ∈ (var x)
+  free-var  : ∀ {x} → x ∈ var x
   free-λ  : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N)
   free-·₁ : ∀ {x L M} → x ∈ L → x ∈ (L · M)
   free-·₂ : ∀ {x L M} → x ∈ M → x ∈ (L · M)
@@ -215,37 +215,44 @@ A term in which no variables appear free is said to be _closed_.
 
 \begin{code}
 _∉_ : Id → Term → Set
-x ∉ M = x ∈ M → ⊥
+x ∉ M = ¬ (x ∈ M)
 
 closed : Term → Set
 closed M = ∀ {x} → x ∉ M
 \end{code}
 
-#### Exercise: 1 star (free-in)
-Prove formally the properties listed above.
+Here are proofs corresponding to the first two examples above.
 
 \begin{code}
-{-
-example-free₁ : x ∈ (λ[ f ∶ (A ⇒ B) ] f · x)
-example-free₁ = ?
-example-free₂ : f ∉ (λ[ f ∶ (A ⇒ B) ] f · x)
-example-free₂ = ?
-example-free₃ : x ∈ (λ[ f ∶ (A ⇒ B) ] f · x)
-example-free₃ = ?
-example-free₄ : f ∈ (λ[ f ∶ (A ⇒ B) ] f · x)
-example-free₄ = ?
--}
+f≢x : f ≢ x
+f≢x ()
+
+example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
+example-free₁ = free-λ f≢x (free-·₂ free-var)
+
+example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x)
+example-free₂ (free-λ f≢x (free-·₁ free-var)) = f≢x refl
+example-free₂ (free-λ f≢x (free-·₂ ()))
 \end{code}
 
 
-If the definition of `_∈_` is not crystal clear to
-you, it is a good idea to take a piece of paper and write out the
-rules in informal inference-rule notation.  (Although it is a
-rather low-level, technical definition, understanding it is
-crucial to understanding substitution and its properties, which
-are really the crux of the lambda-calculus.)
+#### Exercise: 1 star (free-in)
+Prove formally the remaining examples given above.
+
+\begin{code}
+postulate
+  example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
+  example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] var f · var x) · var f)
+  example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
+  example-free₆ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] var f · var x)
+\end{code}
+
+Although `_∈_` may apperar 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