better Agda support for computing reductions

src/Maps.lagda

@@ -36,7 +36,7 @@ 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 Data.String      using (String)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
                              using (_≡_; refl; _≢_; trans; sym)
@@ -54,7 +54,7 @@ we repeat its definition here.
 
 \begin{code}
 data Id : Set where
-  id : String → Id
+  id : ℕ → Id   {- String → Id -}
 \end{code}
 
 We recall a standard fact of logic.
@@ -69,7 +69,7 @@ by deciding equality on the underlying strings.
 
 \begin{code}
 _≟_ : (x y : Id) → Dec (x ≡ y)
-id x ≟ id y with x Data.String.≟ y
+id x ≟ id y with x Data.Nat.≟ y {- x Data.String.≟ y -}
 id x ≟ id y | yes refl  =  yes refl
 id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
   where
@@ -81,9 +81,9 @@ We define some identifiers for future use.
 
 \begin{code}
 x y z : Id
-x = id "x"
-y = id "y"
-z = id "z"
+x = id 0  -- id "x"
+y = id 1  -- id "y"
+z = id 2  -- id "z"
 \end{code}
 
 ## Total Maps

src/Stlc.lagda

@@ -10,7 +10,8 @@ This chapter defines the simply-typed lambda calculus.
 \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.String using (String)
+open import Data.Nat using (ℕ)
 open import Data.Maybe using (Maybe; just; nothing)
 open import Relation.Nullary using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
@@ -44,8 +45,8 @@ data Term : Set where
 Example terms.
 \begin{code}
 f x : Id
-f  =  id "f"
-x  =  id "x"
+f  =  id 0 -- id "f"
+x  =  id 1 -- id "x"
 
 not two : Term 
 not =  λ[ x ∶ 𝔹 ] (if var x then false else true)
@@ -104,6 +105,7 @@ data _⟹_ : Term → Term → Set where
 ## Reflexive and transitive closure
 
 \begin{code}
+{-
 Rel : Set → Set₁
 Rel A = A → A → Set
 
@@ -118,11 +120,52 @@ infix 10 _⟹*_
 
 _⟹*_ : Rel Term
 _⟹*_ = (_⟹_) *
+-}
 \end{code}
 
 ## Notation for setting out reductions
 
 \begin{code}
+infix 10 _⟹*_ 
+infixr 2 _⟹⟨_⟩_
+infix  3 _∎
+
+data _⟹*_ : Term → Term → Set where
+  _∎ : ∀ M → M ⟹* M
+  _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N  
+
+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}
+
+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 _∎
 
@@ -131,17 +174,19 @@ 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
   ∎
 
@@ -161,6 +206,7 @@ reduction₂ =
   ⟹⟨ β𝔹₂ ⟩
     true
   ∎
+-}
 \end{code}
 
 ## Type rules

src/StlcProp.lagda

@@ -128,6 +128,15 @@ progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
 ... | canonical-false = steps β𝔹₂
 \end{code}
 
+This code reads neatly in part because we look at the
+`steps` option before the `done` option. We could, of course,
+look at it the other way around, but then the `...` abbreviation
+no longer works, and we will need to write out all the arguments
+in full. In general, the rule of thumb is to look at the easy case
+(here `steps`) before the hard case (her `done`).
+If you have two hard cases, you will have to expand out `...`
+or introduce subsidiary functions.
+
 #### Exercise: 3 stars, optional (progress_from_term_ind)
 Show that progress can also be proved by induction on terms
 instead of induction on typing derivations.
@@ -140,54 +149,54 @@ postulate
 ## Preservation
 
 The other half of the type soundness property is the preservation
-of types during reduction.  For this, we need to develop some
+of types during reduction.  For this, we need to develop
 technical machinery for reasoning about variables and
 substitution.  Working from top to bottom (from the high-level
 property we are actually interested in to the lowest-level
-technical lemmas that are needed by various cases of the more
-interesting proofs), the story goes like this:
+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 [Stlc]({{ "Stlc" | relative_url }})
+    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
-    `red` rule, whose definition uses the substitution operation.  To see that
+    `β⇒` 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... 
+    does.  So we prove a ... 
 
   - _substitution lemma_, stating that substituting a (closed)
-    term `s` for a variable `x` in a term `t` preserves the type
-    of `t`.  The proof goes by induction on the form of `t` and
+    term `V` for a variable `x` in a term `N` preserves the type
+    of `N`.  The proof goes by induction on the form of `N` and
     requires looking at all the different cases in the definition
-    of substitition.  This time, the tricky cases are the ones for
+    of substitition.  The tricky cases are the ones for
     variables and for function abstractions.  In both cases, we
-    discover that we need to take a term `s` that has been shown
-    to be well-typed in some context `\Gamma` and consider the same
-    term `s` in a slightly different context `\Gamma'`.  For this
+    discover that we need to take a term `V` that has been shown
+    to be well-typed in some context `Γ` and consider the same
+    term in a different context `Γ′`.  For this
     we prove a...
 
   - _context invariance_ lemma, showing that typing is preserved
-    under "inessential changes" to the context `\Gamma`---in
-    particular, changes that do not affect any of the free
-    variables of the term.  And finally, for this, we need a
-    careful definition of...
+    under "inessential changes" to the context---a term `M`
+    well typed in `Γ` is also well typed in `Γ′`, so long as
+    all the free variables of `M` appear in both contexts.
+    And finally, for this, we need a careful definition of ...
 
-  - the _free variables_ of a term---i.e., those variables
+  - _free variables_ of a term---i.e., those variables
     mentioned in a term and not in the scope of an enclosing
     function abstraction binding a variable of the same name.
 
 To make Agda happy, we need to formalize the story in the opposite
-order...
+order.
 
 
 ### Free Occurrences
 
-A variable `x` _appears free in_ a term `M` if `M` contains some
-occurrence of `x` that is not under an abstraction over `x`.
+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:
 
-  - `y` appears free, but `x` does not, in `λ[ x ∶ (A ⇒ B) ] x · y`
-  - both `x` and `y` appear free in `(λ[ x ∶ (A ⇒ B) ] x · y) · x`
-  - no variables appear free in `λ[ x ∶ (A ⇒ B) ] (λ[ y ∶ A ] x · y)`
+  - `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`;
+    note that `f` appears both bound and free in this term
+  - no variables appear free in `λ[ f ∶ (A ⇒ B) ] (λ[ x ∶ A ] f · x)`
 
 Formally:
 
@@ -205,11 +214,30 @@ data _∈_ : Id → Term → Set where
 A term in which no variables appear free is said to be _closed_.
 
 \begin{code}
+_∉_ : Id → Term → Set
+x ∉ M = x ∈ M → ⊥
+
 closed : Term → Set
-closed M = ∀ {x} → ¬ (x ∈ M)
+closed M = ∀ {x} → x ∉ M
 \end{code}
 
 #### Exercise: 1 star (free-in)
+Prove formally the properties listed 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₄ = ?
+-}
+\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

src/extra/Reduction.lagda

@@ -0,0 +1,76 @@
+Old version of reduction
+
+## 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)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+open import Stlc hiding (_⟹*_; _⟹⟨_⟩_; _∎; reduction₁; reduction₂)
+\end{code}
+
+## 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}
+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}