fix to even-odd in Quantifiers

src/Connectives.lagda

@@ -536,7 +536,7 @@ Right identity follows from commutativity of sum and left identity.
   ≃-∎
 \end{code}
 
-## Implication is function
+## Implication is function {#implication}
 
 Given two propositions `A` and `B`, the implication `A → B` holds if
 whenever `A` holds then `B` must also hold.  We formalise implication using

src/Preface.lagda

@@ -74,3 +74,12 @@ Most of the text was written during a sabbatical in the first half of 2018.
 [stump]: http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908
 [wen]: https://github.com/wenkokke
 [phil]: http://homepages.inf.ed.ac.uk/wadler/
+
+## A word on the exercises
+
+Each exercise is followed by a name, which is the name you should use when
+preparing an Agda file that solves the exercise.  Sometimes it is up to you to
+work out the type of the identifier, but sometimes we give it in the exercise.
+In the latter case, the type is bound to an identifier with a capital in its
+name, where the identifier you are to define has a small letter instead.
+

src/Quantifiers.lagda

@@ -213,11 +213,31 @@ Indeed, the converse also holds, and the two together form an isomorphism.
     ; to∘from =  λ{ g → extensionality λ{ (x , y) → refl }}
     }
 \end{code}
-The result can be viewed as a generalisation of currying, and the code to
+The result can be viewed as a generalisation of currying.  Indeed, the code to
-establish the isomorphism is identical.
+establish the isomorphism is identical to what we wrote when discussing
+[implication][implication].
+
+[implication]: Connectives/index.html#implication
+
+### Exercise (`∃-distrib-⊎`)
+
+Show that universals distribute over conjunction.
+\begin{code}
+∃-Distrib-⊎ = ∀ {A : Set} {B C : A → Set} →
+  ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
+\end{code}
+
+### Exercise (`∃×-implies-×∃`)
+
+Show that an existential of conjunctions implies a conjunction of existentials.
+\begin{code}
+∃×-Implies-×∃ = ∀ {A : Set} { B C : A → Set } →
+  ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
+\end{code}
+Does the converse hold? If so, prove; if not, explain why.
 
 
-## Existential examples
+## An existential example
 
 Recall the definitions of `even` and `odd` from Chapter [Relations](Relations).  
 \begin{code}
@@ -238,48 +258,28 @@ We will show that a number is even if and only if it is twice some
 other number, and odd if and only if it is one more than twice
 some other number.  In other words, we will show
 
-    even n   iff   ∃[ m ] (    2 * m ≡ n)
+    even n   iff   ∃[ m ] (    m * 2 ≡ n)
-    odd  n   iff   ∃[ m ] (1 + 2 * m ≡ n)
+    odd  n   iff   ∃[ m ] (1 + m * 2 ≡ n)
 
-First, we need a lemma, which states that twice the successor of `m`
+By convention, one tends to write constant factors first and to put
-is two more than twice `m`.
+the constant term in a sum last. Here we've reversed each of those
-\begin{code}
+conventions, because doing so eases the proof.
-lemma : ∀ (m : ℕ) → 2 * suc m ≡ 2 + 2 * m
-lemma m =
-  begin
-    2 * suc m
-  ≡⟨⟩
-    suc m + (suc m + zero)
-  ≡⟨⟩
-    suc (m + (suc (m + zero)))
-  ≡⟨ cong suc (+-suc m (m + zero)) ⟩
-    suc (suc (m + (m + zero)))
-  ≡⟨⟩
-    2 + 2 * m
-  ∎
-\end{code}
-The lemma is straightforward, and uses the lemma
-`+-suc` from Chapter [Properties](Properties), which
-allows us to simplify `m + suc n` to `suc (m + n)`.
 
 Here is the proof in the forward direction.
 \begin{code}
-even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    2 * m ≡ n)
+even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    m * 2 ≡ n)
-odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + 2 * m ≡ n)
+odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + m * 2 ≡ n)
 
 even-∃ even-zero =  zero , refl
 even-∃ (even-suc o) with odd-∃ o
-...                    | m , refl = suc m , lemma m
+...                    | m , refl = suc m , refl
 
 odd-∃  (odd-suc e)  with even-∃ e
 ...                    | m , refl = m , refl
 \end{code}
 We define two mutually recursive functions. Given
 evidence that `n` is even or odd, we return a
-number `m` and evidence that `2 * m ≡ n` or `1 + 2 * m ≡ n`.
+number `m` and evidence that `m * 2 ≡ n` or `1 + m * 2 ≡ n`.
-(By convention, one tends to put a constant at the
-end of a term, so why have we chosen here
-to write `1 + 2 * m` rather than `2 * m + 1`?)
 We induct over the evidence that `n` is even or odd.
 
 - If the number is even because it is zero, then we return a pair
@@ -287,48 +287,56 @@ consisting of zero and the (trivial) proof that twice zero is zero.
 
 - If the number is even because it is one more than an odd number,
 then we apply the induction hypothesis to give a number `m` and
-evidence that `1 + 2 * m ≡ n`. We return a pair consisting of `suc m`
+evidence that `1 + m * 2 ≡ n`. We return a pair consisting of `suc m`
-and evidence that `2 * (suc m)` ≡ suc n`, which after substituting for
+and evidence that `suc m * 2` ≡ suc n`, which is immediate after
-`n` means we need to show `2 * (suc m) ≡ 2 + 2 * m`, which follows
+substituting for `n`.
-from our lemma.
 
-- If the number is odd because it is the successor of an even
+- If the number is odd because it is the successor of an even number,
-number, then we apply the induction hypothesis to give a number `m`
+then we apply the induction hypothesis to give a number `m` and
-and evidence that `2 * m ≡ n`. We return a pair consisting of `suc m`
+evidence that `m * 2 ≡ n`. We return a pair consisting of `suc m` and
-and evidence that `1 + 2 * m = suc n`, which is immediate
+evidence that `1 + 2 * m = suc n`, which is immediate after
-after substituting for `n`.
+substituting for `n`.
 
 This completes the proof in the forward direction.
 
 Here is the proof in the reverse direction.
 \begin{code}
-∃-even : ∀ {n : ℕ} → ∃[ m ] (   2 * m ≡ n) → even n
+∃-even : ∀ {n : ℕ} → ∃[ m ] (    m * 2 ≡ n) → even n
-∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + 2 * m ≡ n) →  odd n
+∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) →  odd n
 
 ∃-even ( zero , refl)   =  even-zero
-∃-even (suc m , refl) rewrite lemma m  =  even-suc (∃-odd (m , refl))
+∃-even (suc m , refl)   =  even-suc (∃-odd (m , refl))
 
 ∃-odd  (    m , refl)   =  odd-suc (∃-even (m , refl))
 \end{code}
-Given a number that is twice some other number we must show
+Given a number that is twice some other number we must show it is
-it is even, and a number that is one more than twice some other
+even, and a number that is one more than twice some other number we
-number we must show it is odd.  We induct over the evidence
+must show it is odd.  We induct over the evidence of the existential,
-of the existential, and in particular the number that is doubled.
+and in the even case consider the two possibilities for the number
+that is doubled.
 
-- In the even case, if it is `zero`, then we must show `2 * zero` is
+- In the even case for `zero`, we must show `2 * zero` is even, which
-even, which follows by `even-zero`.
+follows by `even-zero`.
 
-- In the even case, if it is `suc n`, then we must show `2 * suc m` is
+- In the even case for `suc n`, we must show `2 * suc m` is even.  The
-even.  After rewriting with our lemma, we must show that `2 + 2 * m`
+inductive hypothesis tells us that `1 + 2 * m` is odd, from which the
-is even. The inductive hypothesis tells us that `1 + 2 * m` is odd,
+desired result follows by `even-suc`.
-from which the desired result follows by `even-suc`.
 
-- In the odd case, then we must show `1 + 2 * suc m` is odd.  The
+- In the odd case, we must show `1 + m * 2` is odd.  The inductive
-inductive hypothesis tell us that `2 * m` is even, from which the
+hypothesis tell us that `m * 2` is even, from which the desired result
-desired result follows by `odd-suc`.
+follows by `odd-suc`.
 
 This completes the proof in the backward direction.
 
+### Exercise (`∃-even′, ∃-odd′`)
+
+How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
+by `2 * m` and `2 * m + 1`?  Rewrite the proofs of `∃-even` and `∃-odd` when
+restated in this way.
+
+
+## Existentials, Universals, and Negation
+
 Negation of an existential is isomorphic to universal
 of a negation.  Considering that existentials are generalised
 disjunction and universals are generalised conjunction, this
@@ -362,23 +370,6 @@ requires extensionality.
 
 
 
-### Exercise (`∃-distrib-⊎`)
-
-Show that universals distribute over conjunction.
-\begin{code}
-∃-Distrib-⊎ = ∀ {A : Set} {B C : A → Set} →
-  ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
-\end{code}
-
-### Exercise (`∃×-implies-×∃`)
-
-Show that an existential of conjunctions implies a conjunction of existentials.
-\begin{code}
-∃×-Implies-×∃ = ∀ {A : Set} { B C : A → Set } →
-  ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
-\end{code}
-Does the converse hold? If so, prove; if not, explain why.
-
 ### Exercise (`∃¬-Implies-¬∀`)
 
 Show `∃[ x ] ¬ B x → ¬ (∀ x → B x)`.

src/extra/EvenOdd3.agda

@@ -0,0 +1,31 @@
+-- Nils' suggestion
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Properties.Simple using (+-suc)
+open import Relation.Nullary using (¬_)
+open import Function using (_∘_; id)
+open import Data.Product using (_×_; _,_; proj₁; proj₂; map; ∃; ∃-syntax)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+
+data even : ℕ → Set
+data odd  : ℕ → Set
+
+data even where
+  even-zero : even zero
+  even-suc  : ∀ {n : ℕ} → odd n → even (suc n)
+
+data odd where
+  odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)
+
+∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ m * 2)
+∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + m * 2)
+
+∃-even even-zero    = zero , refl
+∃-even (even-suc o) with ∃-odd o
+...                    | m , refl = suc m , refl
+
+∃-odd  (odd-suc  e) with ∃-even e
+...                    | m , refl = m , refl