diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 90ff89ed..52b19305 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -452,13 +452,9 @@ Again, it is possible to assign our definition a meaning without resorting to unpermitted circularities. We do so by reducing our definition to equivalent inference rules for judgements about equality. - n : ℕ ------------ zero + n = n - m : ℕ - n : ℕ - p : ℕ m + n = p ------------------- (suc m) + n = suc p diff --git a/src/Properties.lagda b/src/Properties.lagda index 0317e8d3..32a66e52 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -15,20 +15,22 @@ by their name, properties of *inductive datatypes* are proved by Each chapter will begin with a list of the imports we require from the Agda standard library. - + \begin{code} open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_) -open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans) \end{code} Each import consists of the keywords `open` and `import`, followed by the module name, followed by the keyword `using`, followed by the names of each identifier imported from the module, surrounded by -parentheses and separated by semicolons. +parentheses and separated by semicolons. Parentheses and semicolons +are among the few characters that cannot appear in names, so we do not +need extra spaces in the import list. ## Associativity @@ -157,7 +159,6 @@ In order to prove associativity, we take `P m` to be the property Then the appropriate instances of the inference rules, which we must show to hold, become: - n : ℕ p : ℕ ------------------------------- (zero + n) + p ≡ zero + (n + p) @@ -222,9 +223,9 @@ induction hypothesis. 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 `@.(){};_`. @@ -290,15 +291,15 @@ 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 = ? + +-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 + +-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. @@ -319,9 +320,9 @@ the prompt: 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 + +-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: @@ -342,9 +343,9 @@ 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 + +-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: @@ -358,9 +359,9 @@ 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 + +-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: @@ -374,9 +375,9 @@ goal is now trivial: 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 + +-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 @@ -434,7 +435,6 @@ this by induction, we take `P m` to be the property Then the appropriate instances of the inference rules, which we must show to hold, become: - n : ℕ ------------------- zero + n ≡ n + zero @@ -546,29 +546,73 @@ QED. 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 ++-identity : ∀ (n : ℕ) → n + zero ≡ n ++-identity zero = refl ++-identity (suc n) rewrite +-identity 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 ++-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m) ++-suc m zero = refl ++-suc m (suc n) rewrite +-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 ++-comm : ∀ (m n : ℕ) → m + n ≡ n + m ++-comm zero n rewrite +-identity n = refl ++-comm (suc m) n rewrite +-suc m n | +-comm 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. +Here we have renamed Lemma (x) and (xi) to `+-identity` and `+-suc`, +respectively. In the final line, rewriting with two equations is +indicated by separating the two proofs of the relevant equations by a +vertical bar; the rewrite on the left is performed before that on the +right. ## Exercises ++ *Swapping terms*. Show + m + (n + p) ≡ n + (m + p) + for all naturals `m`, `n`, and `p`. No induction is needed, + just apply the previous results which show addition + is associative and commutative. You may need to use + one or more of the following functions from the standard library: + sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m + trans : ∀ {m n p : ℕ} → m ≡ n → n ≡ p → m ≡ p + + Name your proof `+-swap`. + ++ *Multiplication distributes over addition*. Show + + (m + n) * p = m * p + n * p + + for all naturals `m`, `n`, and `p`. Name your proof `*-distrib-+`. + ++ *Multiplication is associative*. Show + + (m * n) * p ≡ m * (n * p) + + for all naturals `m`, `n`, and `p`. Name your proof `*-assoc`. + ++ *Multiplication is commutative*. Show + + m * n = n * m + + for all naturals `m` and `n`. As with commutativity of addition, + you will need to formulate and prove suitable lemmas. + Name your proof `*-comm`. + ++ *Monus from zero* Show + + zero ∸ n = zero + + for all naturals `n`. Did your proof require induction? + Name your proof `0∸n≡0`. + ++ *Associativity of monus with addition* Show + + m ∸ n ∸ p = m ∸ (n + p) + + for all naturals `m`, `n`, and `p`. + Name your proof `∸-+-assoc`. ## Unicode @@ -576,4 +620,3 @@ In this chapter we use the following unicode. ≡ U+2261 IDENTICAL TO (\==) ∀ U+2200 FOR ALL (\forall) - λ U+03BB GREEK SMALL LETTER LAMBDA (\Gl, \lambda) diff --git a/src/Relations.lagda b/src/Relations.lagda index b646c940..9fc00dbd 100644 --- a/src/Relations.lagda +++ b/src/Relations.lagda @@ -11,7 +11,7 @@ the next step is to define relations, such as *less than or equal*. \begin{code} open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_) -open import Properties using (com+; com+zero; com+suc) +open import Properties using (+-comm) open import Relation.Binary.PropositionalEquality using (_≡_; refl) \end{code} @@ -158,13 +158,13 @@ such relations?) The first property to prove about comparison is that it is reflexive: for any natural `n`, the relation `n ≤ n` holds. \begin{code} -refl≤ : ∀ (n : ℕ) → n ≤ n -refl≤ zero = z≤n -refl≤ (suc n) = s≤s (refl≤ n) +≤-refl : ∀ (n : ℕ) → n ≤ n +≤-refl zero = z≤n +≤-refl (suc n) = s≤s (≤-refl n) \end{code} The proof is a straightforward induction on `n`. In the base case, `zero ≤ zero` holds by `z≤n`. In the inductive case, the inductive -hypothesis `refl≤ n` gives us a proof of `n ≤ n`, and applying `s≤s` +hypothesis `≤-refl n` gives us a proof of `n ≤ n`, and applying `s≤s` to that yields a proof of `suc n ≤ suc n`. It is a good exercise to prove reflexivity interactively in Emacs, @@ -177,9 +177,9 @@ The second property to prove about comparison is that it is transitive: for any naturals `m`, `n`, andl `p`, if `m ≤ n` and `n ≤ p` hold, then `m ≤ p` holds. \begin{code} -trans≤ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p -trans≤ z≤n _ = z≤n -trans≤ (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤ m≤n n≤p) +≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p +≤-trans z≤n _ = z≤n +≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p) \end{code} Here the proof is most easily thought of as by induction on the *evidence* that `m ≤ n`, so we have left `m`, `n`, and `p` implicit. @@ -195,20 +195,20 @@ In the inductive case, `m ≤ n` holds by `s≤s m≤n`, so it must be that `m` is `suc m′` and `n` is `suc n′` for some `m′` and `n′`, and `m≤n` is evidence that `m′ ≤ n′`. In this case, the only way that `p ≤ n` can hold is by `s≤s n≤p`, where `p` is `suc p′` for some `p′` and `n≤p` is -evidence that `n′ ≤ p′`. The inductive hypothesis `trans≤ m≤n n≤p` +evidence that `n′ ≤ p′`. The inductive hypothesis `≤-trans m≤n n≤p` provides evidence that `m′ ≤ p′`, and applying `s≤s` to that gives evidence of the desired conclusion, `suc m′ ≤ suc p′`. -The case `trans≤ (s≤s m≤n) z≤n` cannot arise, since the first piece of +The case `≤-trans (s≤s m≤n) z≤n` cannot arise, since the first piece of evidence implies `n` must be `suc n′` for some `n′` while the second implies `n` must be `zero`. Agda can determine that such a case cannot arise, and does not require it to be listed. Alternatively, we could make the implicit parameters explicit. \begin{code} -trans≤′ : ∀ (m n p : ℕ) → m ≤ n → n ≤ p → m ≤ p -trans≤′ zero n p z≤n _ = z≤n -trans≤′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤′ m n p m≤n n≤p) +≤-trans′ : ∀ (m n p : ℕ) → m ≤ n → n ≤ p → m ≤ p +≤-trans′ zero n p z≤n _ = z≤n +≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p) \end{code} One might argue that this is clearer, since it shows us the forms of `m`, `n`, and `p`, or one might argue that the extra length obscures the essence of the @@ -228,9 +228,9 @@ The third property to prove about comparison is that it is antisymmetric: for all naturals `m` and `n`, if both `m ≤ n` and `n ≤ m` hold, then `m ≡ n` holds. \begin{code} -antisym≤ : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n -antisym≤ z≤n z≤n = refl -antisym≤ (s≤s m≤n) (s≤s n≤m) rewrite antisym≤ m≤n n≤m = refl +≤-antisym : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n +≤-antisym z≤n z≤n = refl +≤-antisym (s≤s m≤n) (s≤s n≤m) rewrite ≤-antisym m≤n n≤m = refl \end{code} Again, the proof is by induction over the evidence that `m ≤ n` and `n ≤ m` hold, and so we have left `m` and `n` implicit. @@ -243,7 +243,7 @@ of equivalance, that is, not the reflexivity of comparison.) In the inductive case, `m ≤ n` holds by `s≤s m≤n` and `n ≤ m` holds by `s≤s n≤m`, so it must be that `m` is `suc m′` and `n` is `suc n′`, for some `m′` and `n′`, where `m≤n` is evidence that `m′ ≤ n′` and `n≤m` -is evidence that `n′ ≤ m′`. The inductive hypothesis `antisym≤ m≤n n≤m` +is evidence that `n′ ≤ m′`. The inductive hypothesis `≤-antisym m≤n n≤m` establishes that `m′ ≡ n′`, and rewriting by this equation establishes that `m ≡ n` holds by reflexivity. @@ -254,12 +254,12 @@ the notion that given two propositions either one or the other holds. In Agda, we do so by declaring a suitable inductive type. \begin{code} data _⊎_ : Set → Set → Set where - left : ∀ {A B : Set} → A → A ⊎ B - right : ∀ {A B : Set} → B → A ⊎ B + inj₁ : ∀ {A B : Set} → A → A ⊎ B + inj₂ : ∀ {A B : Set} → B → A ⊎ B \end{code} This tells us that if `A` and `B` are propositions then `A ⊎ B` is also a proposition. Evidence that `A ⊎ B` holds is either of the form -`left a`, where `a` is evidence that `A` holds, or `right b`, where +`inj₁ a`, where `a` is evidence that `A` holds, or `inj₂ b`, where `b` is evidence that `B` holds. We set the precedence of disjunction so that it binds less tightly @@ -275,19 +275,19 @@ The fourth property to prove about comparison is that it is total: for any naturals `m` and `n` either `m ≤ n` or `n ≤ m`, or both if `m` and `n` are equal. \begin{code} -total≤ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m -total≤ zero n = left z≤n -total≤ (suc m) zero = right z≤n -total≤ (suc m) (suc n) with total≤ m n -... | left m≤n = left (s≤s m≤n) -... | right n≤m = right (s≤s n≤m) +≤-total : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m +≤-total zero n = inj₁ z≤n +≤-total (suc m) zero = inj₂ z≤n +≤-total (suc m) (suc n) with ≤-total m n +... | inj₁ m≤n = inj₁ (s≤s m≤n) +... | inj₂ n≤m = inj₂ (s≤s n≤m) \end{code} In this case the proof is by induction over both the first and second arguments. We perform a case analysis: + *First base case*: If the first argument is `zero` and the second argument is `n` then - the left disjunct holds, with `z≤n` as evidence that `zero ≤ n`. + the first disjunct holds, with `z≤n` as evidence that `zero ≤ n`. + *Second base case*: If the first argument is `suc m` and the second argument is `n` then the right disjunct holds, with @@ -295,14 +295,14 @@ and second arguments. We perform a case analysis: + *Inductive case*: If the first argument is `suc m` and the second argument is `suc n`, then the inductive hypothesis - `total≤ m n` establishes one of the following: + `≤-total m n` establishes one of the following: - - The left disjunct of the inductive hypothesis holds with `m≤n` as - evidence that `m ≤ n`, in which case the left disjunct of the + - The first disjunct of the inductive hypothesis holds with `m≤n` as + evidence that `m ≤ n`, in which case the first disjunct of the proposition holds with `s≤s m≤n` as evidence that `suc m ≤ suc n`. - - The right disjunct of the inductive hypothesis holds with `n≤m` as - evidence that `n ≤ m`, in which case the right disjunct of the + - The second disjunct of the inductive hypothesis holds with `n≤m` as + evidence that `n ≤ m`, in which case the second disjunct of the proposition holds with `s≤s n≤m` as evidence that `suc n ≤ suc m`. This is our first use of the `with` clause in Agda. The keyword @@ -314,14 +314,14 @@ sign, and the right-hand side of the equation. Every use of `with` is equivalent to defining a helper function. For example, the definition above is equivalent to the following. \begin{code} -total≤′ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m -total≤′ zero n = left z≤n -total≤′ (suc m) zero = right z≤n -total≤′ (suc m) (suc n) = helper (total≤′ m n) +≤-total′ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m +≤-total′ zero n = inj₁ z≤n +≤-total′ (suc m) zero = inj₂ z≤n +≤-total′ (suc m) (suc n) = helper (≤-total′ m n) where helper : m ≤ n ⊎ n ≤ m → suc m ≤ suc n ⊎ suc n ≤ suc m - helper (left m≤n) = left (s≤s m≤n) - helper (right n≤m) = right (s≤s n≤m) + helper (inj₁ m≤n) = inj₁ (s≤s m≤n) + helper (inj₂ n≤m) = inj₂ (s≤s n≤m) \end{code} This is also our first use of a `where` clause in Agda. The keyword `where` is followed by one or more definitions, which must be @@ -331,17 +331,17 @@ in the right-hand side of the preceding equation (in this case, preceding equation are in scope within the nested definition (in this case, `m` and `n`). -If both arguments are equal, then both the left and right disjuncts +If both arguments are equal, then both the first and second disjuncts hold and we could return evidence of either. In the code above we -always return the left disjunct, but there is a minor variant that -always returns the right disjunct. +always return the first disjunct, but there is a minor variant that +always returns the second disjunct. \begin{code} -total≤″ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m -total≤″ m zero = right z≤n -total≤″ zero (suc n) = left z≤n -total≤″ (suc m) (suc n) with total≤″ m n -... | left m≤n = left (s≤s m≤n) -... | right n≤m = right (s≤s n≤m) +≤-total″ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m +≤-total″ m zero = inj₂ z≤n +≤-total″ zero (suc n) = inj₁ z≤n +≤-total″ (suc m) (suc n) with ≤-total″ m n +... | inj₁ m≤n = inj₁ (s≤s m≤n) +... | inj₂ n≤m = inj₂ (s≤s n≤m) \end{code} @@ -360,11 +360,11 @@ Addition (precedence level 6) binds more tightly than comparison The proof is straightforward using the techniques we have learned, and is best broken into three parts. First, we deal with the special -case where the left arguments of addition are identical. +case of showing addition is monotonic on the right. \begin{code} -mono+≤l : ∀ (m p q : ℕ) → p ≤ q → m + p ≤ m + q -mono+≤l zero p q p≤q = p≤q -mono+≤l (suc m) p q p≤q = s≤s (mono+≤l m p q p≤q) ++-monoʳ-≤ : ∀ (m p q : ℕ) → p ≤ q → m + p ≤ m + q ++-monoʳ-≤ zero p q p≤q = p≤q ++-monoʳ-≤ (suc m) p q p≤q = s≤s (+-monoʳ-≤ m p q p≤q) \end{code} The proof is by induction on the first argument. @@ -374,27 +374,27 @@ The proof is by induction on the first argument. + *Inductive case*: The first argument is `suc m`, in which case `suc m + p ≤ suc m + q` simplifies to `suc (m + p) ≤ suc (m + q)`. - The inductive hypothesis `mono+≤₁ {m} p≤q` establishes that + The inductive hypothesis `+-monoʳ-≤ m p q p≤q` establishes that `m + p ≤ m + q`, from which the desired conclusion follows by an application of `s≤s`. -Second, we deal with the special case where the right arguments -of the addition are identical. This follows from the previous +Second, we deal with the special case of showing addition is +monotonic on the left. This follows from the previous result and the commutativity of addition. \begin{code} -mono+≤r : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p -mono+≤r m n p m≤n rewrite com+ m p | com+ n p = mono+≤l p m n m≤n ++-monoˡ-≤ : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p ++-monoˡ-≤ m n p m≤n rewrite +-comm m p | +-comm n p = +-monoˡ-≤ p m n m≤n \end{code} -Rewriting by `com+ m p` and `com+ n p` converts `m + p ≤ n + p` into -`p + m ≤ p + n`, which is proved by invoking `mono+≤left p m n m≤n`. +Rewriting by `+-comm m p` and `+-comm n p` converts `m + p ≤ n + p` into +`p + m ≤ p + n`, which is proved by invoking `+-monoʳ-≤ p m n m≤n`. Third, we combine the two previous results. \begin{code} mono+≤ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m + p ≤ n + q -mono+≤ m n p q m≤n p≤q = trans≤ (mono+≤r m n p m≤n) (mono+≤l n p q p≤q) +mono+≤ m n p q m≤n p≤q = ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q) \end{code} -Invoking `mono+≤r m n p m≤n` proves `m + p ≤ n + p` and invoking -`mono+≤l n p q p≤q` proves `n + p ≤ n + q`, and combining these with +Invoking `+-monoˡ-≤ m n p m≤n` proves `m + p ≤ n + p` and invoking +`+-monoʳ-≤ n p q p≤q` proves `n + p ≤ n + q`, and combining these with transitivity proves `m + p ≤ n + q`, as was to be shown.