finished proof of assoc+

README.md

@@ -47,7 +47,7 @@ https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
 ## Bindings for Agda mode
 
     ?            create hole
-    {!...!}      create holde
+    {!...!}      create hole
     C-c C-l      reload
     C-c C-c x    split on variable x 
     C-c C-space  fill in hole

index.md

@@ -22,6 +22,7 @@ http://homepages.inf.ed.ac.uk/wadler/
 -->
 
   - [Naturals: Natural numbers]({{ "/Naturals" | relative_url }})
+  - [Properties: Proof by induction]({{ "/Properties" | relative_url }})
   - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
   - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
   - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})

src/Naturals.lagda

@@ -42,9 +42,9 @@ as a pair of inference rules:
     --------
     zero : ℕ
 
-    n : ℕ
+    m : ℕ
     ---------
-    suc n : ℕ
+    suc m : ℕ
 
 And here is the definition in Agda:
 \begin{code}
@@ -58,8 +58,9 @@ and `zero` and `suc` (short for *successor*) are the
 
 Both definitions above tell us the same two things:
 
-1. The term `zero` is a natural number.
++ *Base case*: `zero` is a natural number.
-2. If `n` is a natural number, then the term `suc n` is also a natural number.
++ *Inductive case*: if `m` is a natural number, then `suc m` is also a
+  natural number.
 
 Further, these two rules give the *only* ways of creating natural numbers.
 Hence, the possible natural numbers are
@@ -81,14 +82,14 @@ successor of two; and so on.
 
 ## Unpacking the inference rules
 
-Let's unpack the inference rules.  Each inference rule consists of zero
+Let's unpack the inference rules.  Each inference rule consists of
-or more *judgments* written above a horizontal line, called the *hypotheses*,
+zero or more *judgments* written above a horizontal line, called the
-and a single judgment written below, called the *conclusion*.  
+*hypotheses*, and a single judgment written below, called the
-
+*conclusion*.  The first rule is the base case. It has no hypotheses,
-The first rule has no hypotheses, and the conclusion asserts that zero
+and the conclusion asserts that `zero` is a natural.  The second rule
-is a natural.  The second rule has one hypothesis, which assumes that
+is the inductive case. It has one hypothesis, which assumes that `m`
-`n` is a natural number, and the conclusion asserts that `suc n` is a
+is a natural, and the conclusion asserts that `suc n` is a also a
-natural number.
+natural.
 
 
 ## Unpacking the Agda definition
@@ -112,18 +113,20 @@ corresponding `data` declaration.  The lines
 tell us that `zero` is a natural number and that `suc` takes a natural
 number as argument and returns a natural number.
 
-Here `ℕ` and `→` are unicode symbols that you won't find on your
+You may have notices that `ℕ` and `→` are don't appear on your
-keyboard. At the end of each chapter is a list of all the unicode used
+keyboard.  They are symbols in *unicode*.  At the end of each chapter
-in the chapter, including instructions on how to type them in the
+is a list of all the unicode used in the chapter, including
-Emacs text editor.
+instructions on how to type them in the Emacs text editor using keys
+that are on your keyboard.
 
 
 ## The story of creation
 
 Let's look again at the definition of natural numbers:
 
-1. The term `zero` is a natural number.
++ *Base case*: `zero` is a natural number.
-2. If `n` is a natural number, then the term `suc n` is also a natural number.
++ *Inductive case*: if `m` is a natural number, then `suc m` is also a
+  natural number.
 
 Wait a minute! The second line defines natural numbers
 in terms of natural numbers. How can that posssibly be allowed?
@@ -139,28 +142,27 @@ no natural numbers at all.
 
     -- in the beginning, there are no natural numbers
 
-Now, we apply the rules to all the natural numbers we know about.  One
+Now, we apply the two cases to all the natural numbers we know about.  The
-rule tells us that `zero` is a natural number, so we add it to the set
+base case tells us that `zero` is a natural number, so we add it to the set
-of known natural numbers.  The other rule tells us that if `n` is a
+of known natural numbers.  The inductive case tells us that if `m` is a
-natural number (on the day before today) then `suc n` is also a
+natural number (on the day before today) then `suc m` is also a
 natural number (today).  We didn't know about any natural numbers
-before today, so we don't add any natural numbers of the form `suc n`.
+before today, so the inductive case doesn't apply.
 
     -- on the first day, there is one natural number   
     zero
 
 Then we repeat the process, so on the next day we know about all the
-numbers from the day before, plus any numbers added by the rules.  One
+numbers from the day before, plus any numbers added by the two cases.  The
-rule tells us that `zero` is a natural number, but we already knew
+base case tells us that `zero` is a natural number, but we already knew
-that. But now the other rule tells us that since `zero` was a natural
+that. But now the inductive case tells us that since `zero` was a natural
-number yesterday, `suc zero` is a natural number today.
+number yesterday, then `suc zero` is a natural number today.
 
     -- on the second day, there are two natural numbers
     zero
     suc zero
 
-And we repeat the process again. Once more, one rule tells us what
+And we repeat the process again. Now the inductive case
-we already knew, that `zero` is a natural number.  And now the other rule
 tells us that since `zero` and `suc zero` are both natural numbers, then
 `suc zero` and `suc (suc zero)` are natural numbers. We already knew about
 the first of these, but the second is new.
@@ -179,9 +181,8 @@ You've probably got the hang of it by now.
     suc (suc (suc zero))
 
 The process continues.  On the *n*th day there will be *n* distinct
-natural numbers. Note that in this way, we only talk about finite sets
+natural numbers. Every natural number will appear on some given day.
-of numbers. Every natural number will appear on some given finite
+In particular, the number *n* first appears on day *n+1*. And we
-day. In particular, the number *n* first appears on day *n+1*. And we
 never actually define the set of numbers in terms of itself. Instead,
 we define the set of numbers on day *n+1* in terms of the set of
 numbers on day *n*.
@@ -203,10 +204,10 @@ A philosopher might note that our reference to the first day, second
 day, and so on, implicitly involves an understanding of natural
 numbers.  In this sense, our definition might indeed be regarded as in
 some sense circular.  We won't worry about the philosophy, but are ok
-with taking some intuitive notions---such as counting---as given.
+with taking some intuitive notions--such as counting--as given.
 
 While the natural numbers have been understood for as long as people
-could count, this way of viewing the natural numbers is relatively
+could count, the inductive definition of the natural numbers is relatively
 recent.  It can be traced back to Richard Dedekind's paper "*Was sind
 und was sollen die Zahlen?*" (What are and what should be the
 numbers?), published in 1888, and Giuseppe Peano's book "*Arithmetices
@@ -243,14 +244,13 @@ a machine with 64-bit words.
 ## Operations on naturals are recursive functions
 
 Now that we have the natural numbers, what can we do with them?
-An obvious first step is to define basic operations such as
+For instance, can we define arithmetic operations such as
-addition and multiplication.
+addition and multiplication?
 
 As a child I spent much time memorising tables of addition and
 multiplication.  At first the rules seemed tricky and I would often
-make mistakes.  So it came as a shock to realise that all of addition
+make mistakes.  So it came as a shock to me to realise that all of addition
-can be precisely defined in just a couple of lines, and the same is true of
+and multiplication can be precisely defined in just a couple of lines.
-multiplication.
 
 Here is the definition of addition in Agda:
 \begin{code}

src/Properties.lagda

@@ -4,22 +4,23 @@ layout    : page
 permalink : /Properties
 ---
 
-Now that we've defined the naturals and operations upon them,
+Now that we've defined the naturals and operations upon them, our next
-our next step is to learn how to prove properties that they
+step is to learn how to prove properties that they satisfy.  As hinted
-satisfy.  Unsurprisingly, properties of *inductive datatypes*
+by their name, properties of *inductive datatypes* are proved by
-are proved by *induction*.
+*induction*.
 
 
 ## Imports
 
 Each chapter will begin with a list of the imports we require from the
-Agda standard library.  We will, of course, require the naturals;
+Agda standard library.
+
+<!-- We will, of course, require the naturals;
 everything in the previous chapter is also found in the library module
-`Data.Nat`, so we import the required definitions from there.  We also
+`Data.Nat`, so we import the required definitions from there.
-require propositional equality.
+We also require propositional equality. -->
 
 \begin{code}
-open import Data.Nat using (ℕ; zero; suc)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 \end{code}
 
@@ -54,18 +55,40 @@ variables.
        3 + (4 + 5)
 
 Here we have displayed the computation in tabular form, one term to a
-line.  We will often use such a form.  It is often easiest to read
+line.  It is often easiest to read such computations from the top down
-such computations from the top down until one reaches the simplest
+until one reaches the simplest term (in this case, `12`), and
-possible term (in this case, 12), and then from the bottom up until
+then from the bottom up until one reaches the same term.
-one reaches the same term.
 
-We could go on testing the proposition by choosing other numbers, but---since there are an infinite number of naturals---we will never finish.
+The test reveals that associativity is perhaps not as obvious as first
+it appears.  Why should `7 + 5` be the same as `3 + 9`?  We might want
+to gather more evidence, testing the proposition by choosing other
+numbers.  But---since there are an infinite number of
+naturals---testing can never be complete.  Is there any way we can be
+sure that associativity holds for *all* the natural numbers?
+
+The answer is yes! We can prove a property holds for all naturals using
+*proof by induction*.
 
 
+## Proof by induction
+
+Recall the definition of natural numbers.
+\begin{code}
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+\end{code}
+This tells us that `zero` is a natural--the *base case*--and that if
+`m` is a natural then `suc m` is also a natural---the *inductive
+case*.
+
+Proofs by induction follow the structure of this definition.  To prove
+a property of natural numbers by induction, we need prove two cases.
+First is the *base case*, where we need to show the property holds for
+`zero`.  Second is the *inductive case*, where we assume as the
+*inductive hypothesis* that the property holds for an arbitary natural
+`m` and then show that the property must also hold for `suc m`.
 
-To prove a property of natural numbers by induction, we need to prove two things.
-First, we prove the property holds for `zero`, and secondly we prove that if
-the property holds for an arbitrary natural `m` then it also holds for `suc m`.
 If we write `P m` for a property of `m`, then we can write out the principle
 of induction as an inference rule:
 
@@ -74,13 +97,61 @@ of induction as an inference rule:
     -----------------------------
     ∀ (m : ℕ) → P m
 
-Let's unpack this rule.  The first hypothesis states
+Let's unpack this rule.  The first hypothesis is the base case, and
-that property `P` holds for `zero`.  The second hypothesis states that for all natural
+requires we show that property `P` holds for `zero`.  The second
-numbers `m`, if `P` holds for `m` then `P` also holds for `suc m`.  The conclusion
+hypothesis is the inductive case, and requires that for any natural
-states that for all natural numbers `m` we have that `P` holds for `m`.
+`m` assuming the the induction hypothesis `P` holds for `m` we must
-We call the first hypothesis the *base case*; it requires we show `P zero`.
+then show that `P` also holds for `suc m`.
-We call the second hypothesis the *inductive case*; it requires we assume `P m`, which
+
-we call the *induction hypothesis*, and use it to show `P (suc m)`.
+Why does this work?  Again, it can be explained by a creation story.
+To start with, we know no properties.
+
+    -- in the beginning, no properties are known
+
+Now, we apply the two cases to all the properties we know about.  The
+base case tells us that `P zero` holds, so we add it to the set of
+known properties.  The inductive case tells us that if `P m` holds (on
+the day before today) then `P (suc m)` also holds (today).  We didn't
+know about any properties before today, so the inductive case doesn't
+apply.
+
+    -- on the first day, one property is known
+    P zero
+
+Then we repeat the process, so on the next day we know about all the
+properties from the day before, plus any properties added by the two
+cases.  The base case tells us that `P zero` holds, but we already
+knew that. But now the inductive case tells us that since `P zero`
+held yesterday, then `P (suc zero)` holds today.
+
+    -- on the second day, two properties are known
+    P zero
+    P (suc zero)
+
+And we repeat the process again. Now the inductive case
+tells us that since `P zero` and `P (suc zero)` both hold, then
+`P (suc zero)` and `P (suc (suc zero))` also hold. We already knew about
+the first of these, but the second is new.
+
+    -- on the third day, three properties are known
+    P zero
+    P (suc zero)
+    P (suc (suc zero))
+
+You've probably got the hang of it by now.
+
+    -- on the fourth day, four properties are known
+    P zero
+    P (suc zero)
+    P (suc (suc zero))
+    P (suc (suc (suc zero)))
+
+The process continues.  On the *n*th day there will be *n* distinct
+properties that hold.  The property of every natural number will appear
+on some given day.  In particular, the property `P n` first appears on
+day *n+1*. 
+
+## Our first proof: associativity
 
 In order to prove associativity, we take `P m` to be the property
 
@@ -108,7 +179,7 @@ For the base case, we must show:
     (zero + n) + p ≡ zero + (n + p)
 
 By (i), both sides of the equation simplify to `n + p`, so it holds.
-In tabular form, we write this as follows:
+In tabular form we have:
 
        (zero + n) + p
     ≡    (i)
@@ -116,8 +187,9 @@ In tabular form, we write this as follows:
     ≡    (i)
        zero + (n + p)
 
-It is often easiest to read such proofs down from the top and up from
+Again, it is easiest to read from the top down until one reaches the
-the bottom, meeting in the middle where the two terms are the same.
+simplest term (`n + p`), and then from the bottom up
+until one reaches the same term.
 
 For the inductive case, we assume
 
@@ -141,9 +213,73 @@ these follow from what we assumed.  In tabular form:
     ≡    (ii)
        suc m + (n + p)
 
+Here it is easiest to read from the top down until one reaches the
+simplest term (`suc ((m + n) + p)`), and then from the bottom up until
+one reaches the simplest term (`suc (m + (n + p))`).  In this case,
+the two simplest terms are not the same, but are equated by the
+induction hypothesis.
 
+## Encoding the proof in Agda
 
+We can encode this proof in Agda as follows.
+\begin{code}
+assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+assoc+ zero n p = refl
+assoc+ (suc m) n p rewrite assoc+ m n p = refl
+\end{code}
+Here we have named the proof `assoc+`.  In Agda, identifiers can consist of
+any sequence of characters not including spaces or the characters `@.(){};_`.
 
+Let's unpack this code.  The first line states that we are
+defining the identifier `assoc+` which is a proof of the
+proposition
+
+    ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+
+Such a proof is a function that takes three natural
+numbers---corresponding to `m`, `n`, and `p`---and returns
+a proof of the proposition `(m + n) + p ≡ m + (n + p)`.
+Proof by induction corresponds exactly to a recursive
+definition.  Here we are inducting on the first
+argument `m`, and leaving the other two arguments `n` and `p`
+fixed.
+
+The base case corresponds to instantiating `m` by
+pattern matching on `zero`, so what we are required to
+prove is:
+
+    (zero + n) + p ≡ zero + (n + p)
+
+After simplifying with the definition of addition, this equation
+becomes:
+
+    n + p ≡ n + p
+
+The proof that a term is equal to itself is written `refl`.
+
+The inductive case corresponds to instantiating `m` by `suc zero`,
+so what we are required to prove is:
+
+    (suc m + n) + p ≡ suc m + (n + p)
+
+After simplifying with the definition of addition, this equation
+becomes:
+
+    suc ((m + n) + p) ≡ suc (m + (n + p))
+
+After rewriting with the inductive hypothesis these two terms are
+equal, and the proof is again given by `refl`.
+
+Rewriting by a given equation is indicated by the keyword `rewrite`
+followed by a proof of that equation.  Here the inductive hypothesis
+is not assumed, but instead proved by a recursive invocation of the
+function we are definining, `assoc+ m n p`.  As with addition, this is
+well founded because associativity of larger numbers is defined in
+terms of associativity of smaller numbers.  In this case,
+`assoc (suc m) n p` is defined in terms of `assoc m n p`.
+
+This correspondence between proof by induction and definition by
+recursion is one of the most appealing aspects of Agda.
 
 ## Unicode