From bf6c5a060255f670214762cf4fe1925a716e9148 Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 1 Jan 2018 17:40:30 -0200 Subject: [PATCH] finished proof of assoc+ --- README.md | 2 +- index.md | 1 + src/Naturals.lagda | 78 +++++++++--------- src/Properties.lagda | 188 +++++++++++++++++++++++++++++++++++++------ 4 files changed, 203 insertions(+), 66 deletions(-) diff --git a/README.md b/README.md index 1dd415d6..fd264a21 100644 --- a/README.md +++ b/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 diff --git a/index.md b/index.md index 051d155a..45aca764 100644 --- a/index.md +++ b/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 }}) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index d923fe72..85bd51df 100644 --- a/src/Naturals.lagda +++ b/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. -2. If `n` is a natural number, then the term `suc n` is also a natural number. ++ *Base case*: `zero` is 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 -or more *judgments* written above a horizontal line, called the *hypotheses*, -and a single judgment written below, called the *conclusion*. - -The first rule has no hypotheses, and the conclusion asserts that zero -is a natural. The second rule has one hypothesis, which assumes that -`n` is a natural number, and the conclusion asserts that `suc n` is a -natural number. +Let's unpack the inference rules. Each inference rule consists of +zero or more *judgments* written above a horizontal line, called the +*hypotheses*, and a single judgment written below, called the +*conclusion*. The first rule is the base case. It has no hypotheses, +and the conclusion asserts that `zero` is a natural. The second rule +is the inductive case. It has one hypothesis, which assumes that `m` +is a natural, and the conclusion asserts that `suc n` is a also a +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 -keyboard. At the end of each chapter is a list of all the unicode used -in the chapter, including instructions on how to type them in the -Emacs text editor. +You may have notices that `ℕ` and `→` are don't appear on your +keyboard. They are symbols in *unicode*. At the end of each chapter +is a list of all the unicode used in the chapter, including +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. -2. If `n` is a natural number, then the term `suc n` is also a natural number. ++ *Base case*: `zero` is 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 -rule 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 -natural number (on the day before today) then `suc n` is also a +Now, we apply the two cases 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 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 -rule 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 -number yesterday, `suc zero` is a natural number today. +numbers from the day before, plus any numbers added by the two cases. 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 -And we repeat the process again. Once more, one rule tells us what -we already knew, that `zero` is a natural number. And now the other rule +And we repeat the process again. Now the inductive case 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 -of numbers. Every natural number will appear on some given finite -day. In particular, the number *n* first appears on day *n+1*. And we +natural numbers. Every natural number will appear on some given 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 -addition and multiplication. +For instance, can we define arithmetic operations such as +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 -can be precisely defined in just a couple of lines, and the same is true of -multiplication. +make mistakes. So it came as a shock to me to realise that all of addition +and multiplication can be precisely defined in just a couple of lines. Here is the definition of addition in Agda: \begin{code} diff --git a/src/Properties.lagda b/src/Properties.lagda index fa0454b2..72ac262f 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -4,22 +4,23 @@ layout : page permalink : /Properties --- -Now that we've defined the naturals and operations upon them, -our next step is to learn how to prove properties that they -satisfy. Unsurprisingly, properties of *inductive datatypes* -are proved by *induction*. +Now that we've defined the naturals and operations upon them, our next +step is to learn how to prove properties that they satisfy. As hinted +by their name, properties of *inductive datatypes* are proved by +*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. + + \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 -such computations from the top down until one reaches the simplest -possible term (in this case, 12), and then from the bottom up until -one reaches the same term. +line. It is often easiest to read such computations from the top down +until one reaches the simplest term (in this case, `12`), and +then from the bottom up until 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 -that property `P` holds for `zero`. The second hypothesis states that for all natural -numbers `m`, if `P` holds for `m` then `P` also holds for `suc m`. The conclusion -states that for all natural numbers `m` we have that `P` holds for `m`. -We call the first hypothesis the *base case*; it requires we show `P zero`. -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)`. +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`. + +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 -the bottom, meeting in the middle where the two terms are the same. +Again, it is easiest to read from the top down until one reaches the +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