diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 321343e7..6ab85b7c 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -122,7 +122,7 @@ that are on your keyboard. ## The story of creation -Let's look again at the definition of natural numbers: +Let's look again at the rules that define the natural numbers: + *Base case*: `zero` is a natural number. + *Inductive case*: if `m` is a natural number, then `suc m` is also a @@ -130,7 +130,7 @@ Let's look again at the definition of natural numbers: Wait a minute! The second line defines natural numbers in terms of natural numbers. How can that posssibly be allowed? -Isn't this as useless as claiming "Brexit means Brexit"? +Isn't this as meaningless as claiming "Brexit means Brexit"? In fact, it is possible to assign our definition a meaning without resorting to any unpermitted circularities. Furthermore, we can do so @@ -142,7 +142,7 @@ no natural numbers at all. -- in the beginning, there are no natural numbers -Now, we apply the two cases to all the natural numbers we know about. The +Now, we apply the rules to all the natural numbers we know about. The base case tells us that `zero` is a natural number, so we add it to the set of known natural numbers. The inductive case tells us that if `m` is a natural number (on the day before today) then `suc m` is also a @@ -150,17 +150,17 @@ natural number (today). We didn't know about any natural numbers before today, so the inductive case doesn't apply. -- on the first day, there is one natural number - zero + 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 two cases. The +numbers from the day before, plus any numbers added by the rules. The base case tells us that `zero` is a natural number, but we already knew that. But now the inductive case tells us that since `zero` was a natural number yesterday, then `suc zero` is a natural number today. -- on the second day, there are two natural numbers - zero - suc zero + zero : ℕ + suc zero : ℕ And we repeat the process again. Now the inductive case tells us that since `zero` and `suc zero` are both natural numbers, then @@ -168,17 +168,17 @@ tells us that since `zero` and `suc zero` are both natural numbers, then the first of these, but the second is new. -- on the third day, there are three natural numbers - zero - suc zero - suc (suc zero) + zero : ℕ + suc zero : ℕ + suc (suc zero) : ℕ You've probably got the hang of it by now. -- on the fourth day, there are four natural numbers - zero - suc zero - suc (suc zero) - suc (suc (suc zero)) + zero : ℕ + suc zero : ℕ + suc (suc zero) : ℕ + suc (suc (suc zero)) : ℕ The process continues. On the *n*th day there will be *n* distinct natural numbers. Every natural number will appear on some given day. @@ -200,14 +200,19 @@ we would have no numbers in the beginning, and still no numbers on the second day, and on the third, and so on. An inductive definition lacking a base case is useless, as in the phrase "Brexit means Brexit". -A philosopher might note that our reference to the first day, second -day, and so on, implicitly involves an understanding of natural + +## Philosophy and history + +A philosopher might observe 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. +some sense circular. We need not let this circularity disturb us. +Everyone possesses a good informal understanding of the natural +numbers, which we may take as a foundation for their formal +description. While the natural numbers have been understood for as long as people -could count, the inductive definition of the natural numbers is relatively +can 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 @@ -457,52 +462,58 @@ definition to equivalent inference rules for judgements about equality. Here we assume we have already defined the infinite set of natural numbers, specifying the meaning of the judgment `n : ℕ`. The first -inference rule asserts that if `n` is a natural number then adding -zero to it gives `n`, and the second rule asserts that if adding `m` -and `n` gives `p`, then adding `suc m` and `n` gives `suc p`. +inference rule is the base case, and corresponds to line (i) of the +definition. It asserts that if `n` is a natural number then adding +zero to it gives `n`. The second inference rule is the inductive +case, and corresponds to line (ii) of the definition. It asserts that +if adding `m` and `n` gives `p`, then adding `suc m` and `n` gives +`suc p`. -Now we can resort to a similar creation story, where now we are +Again we resort to a creation story, where this time we are concerned with judgements about addition. - -- in the beginning, we know nothing about addition + -- in the beginning, we know nothing about addition Now, we apply the rules to all the judgment we know about. -One rule tells us that `zero + n = n` for every natural `n`, -so we add all those equations. The other rule tells us that if +The base case tells us that `zero + n = n` for every natural `n`, +so we add all those equations. The inductive case tells us that if `m + n = p` (on the day before today) then `suc m + n = suc p` (today). We didn't know any equations about addition before today, -so that rule doesn't give us any equations. +so that rule doesn't give us any new equations. - -- on the first day, we know about addition of 0 - 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... + -- on the first day, we know about addition of 0 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... Then we repeat the process, so on the next day we know about all the -equations from the day before, plus any equations added by the rules. One -rule tells us that `zero + n = n` for every natural `n`, but we already knew -that. But now the other rule tells us that for every equation `m + n = p` -that we knew yesterday, we know `suc m + n = suc p` today. +equations from the day before, plus any equations added by the rules. +The base case tells us nothing new, but now the inductive case adds +more equations. - -- on the second day, we know about addition of 0 and 1 - 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... - 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 ... + -- on the second day, we know about addition of 0 and 1 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ... + 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ... And we repeat the process again. - -- on the third day, we know about addition of 0, 1, and 2 - 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... - 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 ... - 2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 ... + -- on the third day, we know about addition of 0, 1, and 2 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ... + 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ... + 2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 2 + 3 = 5 ... You've probably got the hang of it by now. -The process continues. On the *m*th day we will know all the equations -where the first number is less than *m*. As before, there is both a -base case (line (i) of the definition) and an inductive case (line -(ii)). + -- on the fourth day, we know about addition of 0, 1, 2, and 3 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ... + 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ... + 2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 2 + 3 = 5 ... + 3 + 0 = 3 3 + 1 = 4 3 + 2 = 5 3 + 3 = 6 ... -As we can see, the reasoning that justifies inductive and -recursive definitions is quite similar, and they might be considered -as two sides of the same coin. +The process continues. On the *m*th day we will know all the +equations where the first number is less than *m*. + +As we can see, the reasoning that justifies inductive and recursive +definitions is quite similar. They might be considered two sides of +the same coin. ## Precedence @@ -560,6 +571,11 @@ In this chapter we use the following. → U+2192 RIGHTWARDS ARROW (\to, \r) ∸ U+2238 DOT MINUS (\.-) -Each line consists of the unicode character (ℕ), the corresponding +Each line consists of the Unicode character (ℕ), the corresponding code point (U+2115), the name of the character (DOUBLE-STRUCK CAPITAL N), and the sequence to type into Emacs to generate the character (\bN). + +The command \r is a little different to the others, because it gives +access to a wide variety of Unicode arrows. After typing \r, one can access +the many available arrows by using the left, right, up, and down +keys on the keyboard to navigate. diff --git a/src/Properties.lagda b/src/Properties.lagda index 6163c19b..4db9e72e 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -84,31 +84,33 @@ 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`. +First is the *base case*, where we show the property holds for `zero`. +Second is the *inductive case*, where we assume the the property holds for +an arbitary natural `m` (we call this the *inductive hypothesis*), and +then show that the property must also hold 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: +If we write `P m` for a property of `m`, then what we need to +demonstrate are the following two inference rules: + ------ P zero - ∀ (m : ℕ) → P m → P (suc m) - ----------------------------- - ∀ (m : ℕ) → P m -Let's unpack this rule. The first hypothesis is the base case, and -requires we show that property `P` holds for `zero`. The second -hypothesis is the inductive case, and requires that for any natural -`m` assuming the the induction hypothesis `P` holds for `m` we must -then show that `P` also holds for `suc m`. + P m + --------- + P (suc m) + +Let's unpack these rules. The first rule is the base case, and +requires we show that property `P` holds for `zero`. The second rule +is the inductive case, and requires we show that if we assume the +inductive hypothesis, that `P` holds for `m`, then it follows that +`P` also holds for `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 +Now, we apply the two rules 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 @@ -119,8 +121,8 @@ apply. 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 +properties from the day before, plus any properties added by the rules. +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. @@ -157,14 +159,18 @@ In order to prove associativity, we take `P m` to be the property (m + n) + p ≡ m + (n + p) -Then the appropriate instance of the inference rule becomes: +Then the appropriate instances of the inference rules, which +we must show to hold, become: + n : ℕ p : ℕ + ------------------------------- (zero + n) + p ≡ zero + (n + p) - ∀ (m : ℕ) → (m + n) + p ≡ m + (n + p) → (suc m + n) + p ≡ (suc m + n) + p - ----------------------------------------------------------------------------- - ∀ (m : ℕ) → (m + n) + p ≡ m + (n + p) -In the inference rule, `n` and `p` are any arbitary natural numbers, so when we + (m + n) + p ≡ m + (n + p) + --------------------------------- + (suc m + n) + p ≡ (suc m + n) + p + +In the inference rules, `n` and `p` are any arbitary natural numbers, so when we are done with the proof we know it holds for any `n` and `p` as well as any `m`. Recall the definition of addition. @@ -221,11 +227,11 @@ induction hypothesis. ## Encoding the proof in Agda -We can encode this proof in Agda as follows. +We 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 +-- 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 `@.(){};_`. @@ -236,13 +242,15 @@ 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 upside down A is pronounced "for all", and the proposition +asserts that for all natural numbers `m`, `n`, and `p` that +the equations `(m + n) + p ≡ m + (n + p)` holds. Such a proof +is a function that accepts three natural numbers---corresponding to +to `m`, `n`, and `p`---and returns a proof of the equation. + +Proof by induction corresponds exactly to a recursive definition. +Here we are induct on the first argument `m`, and leave 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 @@ -269,18 +277,303 @@ becomes: 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`. +followed by a proof of that equation. -This correspondence between proof by induction and definition by +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 proved in terms of associativity of smaller numbers. +In this case, `assoc (suc m) n p` is proved using `assoc m n p`. + +The correspondence between proof by induction and definition by recursion is one of the most appealing aspects of Agda. + +## Building proofs interactively + +Agda is designed to be used with the Emacs text editor, and the two +in combination provide features that help to create proofs interactively. + +Begin by typing + + assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) + assoc+ m n p = ? + +The question mark indicates that you would like Agda to help with +filling in that part of the code. If you type `^C ^L` (control-C +followed by control-L), the question mark will be replaced. + + assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) + assoc+ m n p = { }0 + +The empty braces are called a *hole*, and 0 is a number used for +referring to the hole. The hole may display highlighted in green. +Emacs will also create a new window at the bottom of the screen +displaying the text + + ?0 : ((m + n) + p) ≡ (m + (n + p)) + +This indicates that hole 0 is to be filled in with a proof of +the stated judgement. + +We wish to prove the proposition by induction on `m`. More +the cursor into the hole and type `^C ^C`. You will be given +the prompt: + + pattern variables to case: + +Typing `m` will cause a split on that variable, resulting +in an update to the code. + + assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) + assoc+ zero n p = { }0 + assoc+ (suc m) n p = { }1 + +There are now two holes, and the window at the bottom tells you what +each is required to prove: + + ?0 : ((zero + n) + p) ≡ (zero + (n + p)) + ?1 : ((suc m + n) + p) ≡ (suc m + (n + p)) + +Going into hole 0 and typing `^C ^,` will display the text: + + Goal: (n + p) ≡ (n + p) + ———————————————————————————————————————————————————————————— + p : ℕ + n : ℕ + +This indicates that after simplification the goal for hole 0 is as +stated, and that variables `p` and `n` of the stated types are +available to use in the proof. The proof of the given goal is +trivial, and going into the goal and typing `^C ^R` will fill it in, +renumbering the remaining hole to 0: + + assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) + assoc+ zero n p = refl + assoc+ (suc m) n p = { }0 + +Going into the new hold 0 and typing `^C ^,` will display the text: + + Goal: suc ((m + n) + p) ≡ suc (m + (n + p)) + ———————————————————————————————————————————————————————————— + p : ℕ + n : ℕ + m : ℕ + +Again, this gives the simplified goal and the available variables. +In this case, we need to rewrite by the induction +hypothesis, so let's edit the text accordingly: + + 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 = { }0 + +Going into the remaining hole and typing `^C ^,` will show the +goal is now trivial: + + Goal: suc (m + (n + p)) ≡ suc (m + (n + p)) + ———————————————————————————————————————————————————————————— + p : ℕ + n : ℕ + m : ℕ + +The proof of the given goal is trivial, and going into the goal and +typing `^C ^R` will fill it in, completing the proof: + + 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 + + +## Creation, one last time + +Again, it may be helpful to view the recursive definition as +a creation story. This time we are concerned with judgements +asserting associativity. + + -- in the beginning, we know nothing about associativity + +Now, we apply the rules to all the judgements we know about. The base +case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural +`n` and `p`. The inductive case tells us that if `(m + n) + p ≡ m + +(n + p)` (on the day before today) then `(suc m + n) + p ≡ suc m + (n ++ p)` (today). We didn't know any judgments about associativity +before today, so that rule doesn't give us any new judgments. + + -- on the first day, we know about associativity of 0 + (0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ... + +Then we repeat the process, so on the next day we know about all the +judgements from the day before, plus any judgements added by the rules. +The base case tells us nothing new, but now the inductive case adds +more judgements. + + -- on the second day, we know about associativity of 0 and 1 + (0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ... + (1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ... + +And we repeat the process again. + + -- on the third day, we know about associativity of 0, 1, and 2 + (0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ... + (1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ... + (2 + 0) + 0 ≡ 2 + (0 + 0) ... (2 + 4) + 5 ≡ 2 + (4 + 5) ... + +You've probably got the hang of it by now. + + -- on the fourth day, we know about associativity of 0, 1, 2, and 3 + (0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ... + (1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ... + (2 + 0) + 0 ≡ 2 + (0 + 0) ... (2 + 4) + 5 ≡ 2 + (4 + 5) ... + +The process continues. On the *m*th day we will know all the +judgements where the first number is less than *m*. + + +## Our second proof: commutativity + +Another important property of addition is that it is commutative. To show +this by induction, we take `P m` to be the property + + m + n ≡ n + m + +Then the appropriate instances of the inference rules, which +we must show to hold, become: + + n : ℕ + ------------------- + zero + n ≡ n + zero + + m + n ≡ n + m + --------------------- + suc m + n ≡ n + suc m + +In the inference rules, `n` is any arbitary natural number, so when we +are done with the proof we know it holds for any `n` as well as any `m`. + +By equation (i) of the definition of addition, the left-hand side of +the conclusion of the base case simplifies to `n`, so the base case +will hold if we can show + + n + zero ≡ n -- (x) + +By equation (ii) of the definition of addition, the left-hand side of +the conclusion of the inductive case simplifies to `suc (m + n)`, so +the inductive case will hold if we can show + + n + suc m ≡ suc (n + m) -- (xi) + +and then apply the inductive hypothesis to rewrite `m + n` to `n + m`. +We use induction two more times, on `n` this time rather than `m`, to +show both (x) and (xi). + +Here is the proof written out in full, using tabular form. + +Proposition. + + m + n ≡ n + m + +Proof. By induction on `m`. + +Base case. + + zero + n + ≡ (i) + n + ≡ (x) + n + zero + +Inductive case. + + suc m + n + ≡ (ii) + suc (m + n) + ≡ (inductive hypothesis) + suc (n + m) + ≡ (xi) + n + suc m + +QED. + +As with other tabular prooofs, it is best understood by reading from top +down and bottom up and meeting in the middle. + +We now prove each of the two required lemmas, (x) and (xi). + +Lemma (x). + + n + zero ≡ n + +Proof. By induction on `n`. + +Base case. + + zero + zero + ≡ (i) + zero + +Inductive case. + + suc n + zero + ≡ (ii) + suc (n + zero) + ≡ (inductive hypothesis) + suc n + +QED. + +Lemma (xi). + + n + suc m ≡ suc (n + m) + +Proof. By induction on `n`. + +Base case. + + zero + suc m + ≡ (i) + suc m + ≡ (i) + suc (zero + m) + +Inductive case. + + suc n + suc m + ≡ (ii) + suc (n + suc m) + ≡ (inductive hypothesis) + suc (suc (n + m)) + ≡ (ii) + suc (suc n + m) + +QED. + +## Encoding the proofs in Agda + +These proofs can be encoded concisely in Agda. +\begin{code} +com+zero : ∀ (n : ℕ) → n + zero ≡ n +com+zero zero = refl +com+zero (suc n) rewrite com+zero n = refl + +com+suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m) +com+suc m zero = refl +com+suc m (suc n) rewrite com+suc m n = refl + +com : ∀ (m n : ℕ) → m + n ≡ n + m +com zero n rewrite com+zero n = refl +com (suc m) n rewrite com+suc m n | com m n = refl +\end{code} +Here we have renamed Lemma (x) and (xi) to `com+zero` and `com+suc`, +respectively. In the final line, rewriting with two equations +(lemma (xi) and the inductive hypothesis) is indicated by +separating the two proofs of the relevant equations by a vertical bar; +the rewrites on the left is performed before that on the right. + + + + ## Unicode In this chapter we use the following unicode.