completed pass over Quantifiers

src/Connectives.lagda

@@ -694,7 +694,7 @@ is the same as the assertion that if `A` holds then `B` holds and if
 `A` holds then `C` holds.  The proof of left inverse requires both extensionality
 and the rule `η-×` for products.
 \begin{code}
-→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ ((A → B) × (A → C))
+→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
 →-distrib-× =
   record
     { to      = λ{ f → ( (λ{ x → proj₁ (f x) }) , (λ{ y → proj₂ (f y)}) ) }
@@ -710,7 +710,7 @@ and the rule `η-×` for products.
 Products distributes over sum, up to isomorphism.  The code to validate
 this fact is similar in structure to our previous results.
 \begin{code}
-×-distrib-⊎ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
+×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
 ×-distrib-⊎ =
   record
     { to      = λ{ ((inj₁ x) , z) → (inj₁ (x , z)) 
@@ -730,7 +730,7 @@ this fact is similar in structure to our previous results.
 
 Sums do not distribute over products up to isomorphism, but it is an embedding.
 \begin{code}
-⊎-distrib-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≲ ((A ⊎ C) × (B ⊎ C))
+⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
 ⊎-distrib-× =
   record
     { to      = λ{ (inj₁ (x , y)) → (inj₁ x , inj₁ y)
@@ -763,6 +763,16 @@ gives rise to an isomorphism, while the second only gives rise to an
 embedding, revealing a sense in which one of these laws is "more
 true" than the other.
 
+
+### Exercise (`×⊎-implies-⊎×`)
+
+Show that a conjunct of disjuncts implies a disjunct of conjuncts.
+\begin{code}
+×⊎-Implies-⊎× = ∀ {A B C D : Set} → (A ⊎ B) × (C ⊎ D) → (A × C) ⊎ (B × D)
+\end{code}
+Does the converse hold? If so, prove; if not, explain why.
+
+
 ### Exercise (`⇔-refl`, `⇔-sym`, `⇔-trans`)
 
 Define equivalence of propositions (also known as "if and only if") as follows.

src/Isomorphism.lagda

@@ -35,6 +35,7 @@ then applies `g`.
 In set theory, two sets are isomorphic if they are in one-to-one correspondence.
 Here is a formal definition of isomorphism.
 \begin{code}
+infix 0 _≃_
 record _≃_ (A B : Set) : Set where
   field
     to   : A → B
@@ -216,6 +217,7 @@ correspondence between the second type and the first.
 
 Here is the formal definition of embedding.
 \begin{code}
+infix 0 _≲_
 record _≲_ (A B : Set) : Set where
   field
     to      : A → B

src/Quantifiers.lagda

@@ -93,7 +93,7 @@ Show that a disjunction of universals implies a universal of disjunctions.
 ⊎∀-Implies-∀⊎ = ∀ {A : Set} { B C : A → Set } →
   (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x)  →  ∀ (x : A) → B x ⊎ C x
 \end{code}
-Does the converse also hold? If so, prove; if not, explain why.
+Does the converse hold? If so, prove; if not, explain why.
 
 
 ## Existentials
@@ -133,24 +133,29 @@ are provided by the evidence for `∃ (λ (x : A) → B x)`.
 
 Agda makes it possible to define our own syntactic abbreviations.
 \begin{code}
-syntax ∃ {A} (λ x → B) = ∃[ x ∈ A ] B
+syntax ∃ (λ x → B) = ∃[ x ] B
 \end{code}
-This allows us to write `∃[ x ∈ A ] (B x)` in place of
+This allows us to write `∃[ x ] (B x)` in place of `∃ (λ x → B x)`.
-`∃ (λ (x : A) → B x)`.
 
-As an example, recall the definitions of `even` from
+As an example, recall the definitions of `even` and `odd` from
 Chapter [Relations](Relations).  
 \begin{code}
-data even : ℕ → Set where
+data even : ℕ → Set
-  ev0 : even zero
+data odd  : ℕ → Set
-  ev+2 : ∀ {n : ℕ} → even n → even (suc (suc n))
+
+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)
 \end{code}
-A number is even if it is zero, or if it is two
+A number is even if it is zero or the successor of an odd number, and
-greater than an even number.
+odd if it the successor of an even number.
 
 We will show that a number is even if and only if it is twice some
-other number.  That is, number `n` is even if and only if there exists
+other number, and odd if and only if it is one more than twice
-a number `m` such that twice `m` is `n`.
+some other number.
 
 First, we need a lemma, which allows us to
 simplify twice the successor of `m` to two
@@ -176,47 +181,70 @@ allows us to simplify `m + suc n` to `suc (m + n)`.
 
 Here is the proof in the forward direction.
 \begin{code}
-ev-ex : ∀ {n : ℕ} → even n → ∃[ m ∈ ℕ ] (2 * m ≡ n)
+even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    2 * m ≡ n)
-ev-ex ev0 =  (zero , refl)
+odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + 2 * m ≡ n)
-ev-ex (ev+2 ev) with ev-ex ev
+
-... | (m , refl) = (suc m , lemma m)
+even-∃ even-zero =  zero , refl
+even-∃ (even-suc o) with odd-∃ o
+...                    | m , refl = suc m , lemma m
+
+odd-∃  (odd-suc e)  with even-∃ e
+...                    | m , refl = m , refl
 \end{code}
-Given an even number, we must show it is twice some
+We define two mutually recursive functions. Given
-other number.  The proof is a function, which
+evidence that `n` is even or odd, we return a
-given a proof that `n` is even
+number `m` and evidence that `2 * m ≡ n` or `1 + 2 * m ≡ n`.
-returns a pair consisting of `m` and a proof
+(By convention, one tends to put a constant at the
-that twice `m` is `n`.  The proof is by induction over
+end of a term, so why have we chosen here
-the evidence that `n` is even.
+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
 consisting of zero and the (trivial) proof that twice zero is zero.
 
-- If the number is even because it is two more than another even
+- If the number is even because it is one more than an odd number,
-number `n`, then we apply the induction hypothesis, giving us a number
+then we apply the induction hypothesis to give a number `m` and
-`m` and a proof that `2 * m ≡ n`, which we match against `refl`.  We
+evidence that `1 + 2 * m ≡ n`. We return a pair consisting of `suc m`
-return a pair consisting of `suc m` and a proof that `2 * suc m ≡ suc
+and evidence that `2 * (suc m)` ≡ suc n`, which after substituting for
-(suc n)`, which follows from `2 * m ≡ n` and the lemma.
+`n` means we need to show `2 * (suc m) ≡ 2 + 2 * m`, which follows
+from our lemma.
+
+- If the number is odd because it is the successor of an even
+number, then we apply the induction hypothesis to give a number `m`
+and evidence that `2 * m ≡ n`. We return a pair conisting of `suc m`
+and evidence that `1 + 2 * m = suc n`, which is immediate
+after substituting for `n`.
+
+This completes the proof in the forward direction.
 
 Here is the proof in the reverse direction.
 \begin{code}
-ex-ev : ∀ {n : ℕ} → ∃[ m ∈ ℕ ] (2 * m ≡ n) → even n
+∃-even : ∀ {n : ℕ} → ∃[ m ] (   2 * m ≡ n) → even n
-ex-ev (zero , refl) = ev0
+∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + 2 * m ≡ n) →  odd n
-ex-ev (suc m , refl) rewrite lemma m = ev+2 (ex-ev (m , refl))
+
+∃-even ( zero , refl)                  =  even-zero
+∃-even (suc m , refl) rewrite lemma m  =  even-suc (∃-odd (m , refl))
+
+∃-odd  (    m , refl)                  =  odd-suc (∃-even (m , refl))
 \end{code}
-Given a number that is twice some other number,
+Given a number that is twice some other number we must show
-we must show that it is even.  The proof is a function,
+it is even, and a number that is one more than twice some other
-which given a number `m` and a proof that `n` is twice `m`,
+number we must show it is odd.  We induct over the evidence
-returns a proof that `n` is even.  The proof is by induction
+of the existential, and in particular the number that is doubled.
-over the number `m`.
 
-- If it is zero, then we must show that twice zero is even,
+- In the even case, if it is `zero`, then we must show `2 * zero` is
-which follows by rule `ev0`. 
+even, which follows by `even-zero`.
 
-- If it is `suc m`, then we must show that `2 * suc m` is
+- In the even case, if it is `suc n`, then we must show `2 * suc m` is
-even.  After rewriting with our lemma, we must show that
+even.  After rewriting with our lemma, we must show that `2 + 2 * m`
-`suc (suc (2 * m))` is even.  The inductive hypothesis tells
+is even. The inductive hypothesis tells us that `1 + 2 * m` is odd,
-us `2 * m` is even, from which the desired result follows
+from which the desired result follows by `even-suc`.
-by rule `ev+2`.
+
+- In the odd case, then we must show `1 + 2 * suc m` is odd.  The
+inductive hypothesis tell us that `2 * m` is even, from which the
+desired result follows by `odd-suc`.
+
+This completes the proof in the backward direction.
 
 Negation of an existential is isomorphic to universal
 of a negation.  Considering that existentials are generalised
@@ -224,44 +252,67 @@ disjuntion and universals are generalised conjunction, this
 result is analogous to the one which tells us that negation
 of a disjuntion is isomorphic to a conjunction of negations.
 \begin{code}
-¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ∈ A ] B x) ≃ ∀ (x : A) → ¬ B x
+¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x
 ¬∃∀ =
   record
-    { to      =  λ { ¬∃bx x bx → ¬∃bx (x , bx) }
+    { to      =  λ{ ¬∃xy x y → ¬∃xy (x , y) }
-    ; from    =  λ { ∀¬bx (x , bx) → ∀¬bx x bx }
+    ; from    =  λ{ ∀¬xy (x , y) → ∀¬xy x y }
-    ; from∘to =  λ { ¬∃bx → extensionality (λ { (x , bx) → refl }) } 
+    ; from∘to =  λ{ ¬∃xy → extensionality λ{ (x , y) → refl } } 
-    ; to∘from =  λ { ∀¬bx → refl } 
+    ; to∘from =  λ{ ∀¬xy → refl } 
     }
 \end{code}
-In the `to` direction, we are given a value `¬∃bx` of type
+In the `to` direction, we are given a value `¬∃xy` of type
-`¬ ∃ (λ (x : A) → B x)`, and need to show that given a value
+`¬ ∃[ x ] B x`, and need to show that given a value
-`x` of type `A` that `¬ B x` follows, in other words, from
+`x` that `¬ B x` follows, in other words, from
-a value `bx` of type `B x` we can derive false.  Combining
+a value `y` of type `B x` we can derive false.  Combining
-`x` and `bx` gives us a value `(x , bx)` of type `∃ (λ (x : A) → B x)`,
+`x` and `y` gives us a value `(x , y)` of type `∃[ x ] B x`,
-and applying `¬∃bx` to that yields a contradiction.
+and applying `¬∃xy` to that yields a contradiction.
 
-In the `from` direction, we are given a value `∀¬bx` of type
+In the `from` direction, we are given a value `∀¬xy` of type
-`∀ (x : A) → ¬ B x`, and need to show that from a value `(x , bx)`
+`∀ x → ¬ B x`, and need to show that from a value `(x , y)`
-of type `∃ (λ (x : A) → B x)` we can derive false.  Applying `∀¬bx`
+of type `∃[ x ] B x` we can derive false.  Applying `∀¬xy`
-to `x` gives a value of type `¬ B x`, and applying that to `bx` yields
+to `x` gives a value of type `¬ B x`, and applying that to `y` yields
 a contradiction.
 
 The two inverse proofs are straightforward, where one direction
 requires extensionality.
 
-*Exercise* Show `∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x)`.
+### 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)`.
+
+Does the converse hold? If so, prove; if not, explain why.
+
 
 ## Standard Prelude
 
 Definitions similar to those in this chapter can be found in the standard library.
 \begin{code}
-import Data.Product using (∃)
+import Data.Product using (∃;_,_)
 \end{code}
 
+
 ## Unicode
 
-This chapter introduces the following unicode.
+This chapter uses the following unicode.
 
-    ≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
+    ∃  U+2203  THERE EXISTS (\ex, \exists)
 
 

src/Relations.lagda

@@ -540,7 +540,7 @@ data odd where
   odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)
 \end{code}
 A number is even if it is zero or the successor of an odd number,
-and a number is odd if it is the successor of an even number.
+and odd if it is the successor of an even number.
 
 This is our first use of a mutually recursive datatype declaration.
 Since each identifier must be defined before it is used, we first

src/extra/DecidableBroken.agda

@@ -14,22 +14,16 @@ suc m ≤? suc n with m ≤? n
 ... | yes m≤n = yes (s≤s m≤n)
 ... | no ¬m≤n = no λ{ (s≤s m≤n) → ¬m≤n m≤n }
 
-_ : Dec (2 ≤ 4)
-_ = 2 ≤? 4   -- yes (s≤s (s≤s z≤n))
-
 _ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
 _ = refl
 
-_ : Dec (4 ≤ 2)
+_ : 4 ≤? 2 ≡ no {!!}
-_ = 4 ≤? 2   -- no λ{(s≤s (s≤s ()))}
-
-_ : 4 ≤? 2 ≡ no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) m≤n }) m≤n })
 _ = refl
 
 {-
-/Users/wadler/sf/src/extra/DecidableBroken.agda:27,5-9
+Using ^C ^N, the term 
-(λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n }) x !=
+  4 ≤? 2
-(λ { (s≤s m≤n) → _34 m≤n }) x of type .Data.Empty.⊥
+evaluates to
-when checking that the expression refl has type
+  no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n })
-(4 ≤? 2) ≡ no (λ { (s≤s m≤n) → _34 m≤n })
+The 1 is spurious.
 -}

src/extra/RewriteWTF.agda

@@ -1,5 +1,6 @@
 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 Data.Product using (∃; ∃-syntax; _,_)
@@ -14,23 +15,46 @@ data even where
 data odd where
   odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)
 
-∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ 2 * m)
+lemma : ∀ (m : ℕ) → 2 * suc m ≡ suc (suc (2 * m))
-∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + 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)))
+  ≡⟨⟩
+    suc (suc (2 * m))
+  ∎
+
+∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (2 * m ≡ n)
+∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + 2 * m ≡ n)
 
 ∃-even even-zero =  zero , refl
 ∃-even (even-suc o) with ∃-odd o
-...                    | m , eqn rewrite eqn | sym (+-suc m (m + 0)) = suc m , refl
+...                    | m , refl = suc m , lemma m
 
 ∃-odd  (odd-suc e)  with ∃-even e
-...                    | m , eqn rewrite eqn = m , refl
+...                    | m , refl = m , refl
 
 ∃-even′ : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ 2 * m)
 ∃-odd′  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + 2 * m)
 
 ∃-even′ even-zero =  zero , refl
 ∃-even′ (even-suc o) with ∃-odd′ o
-...                     | m , eqn rewrite eqn | +-suc m (m + 0) = suc m , ?
+...                     | m , eqn rewrite eqn | +-suc m (m + 0) = suc m , {!!}
 
 ∃-odd′  (odd-suc e)  with ∃-even′ e
 ...                     | m , eqn rewrite eqn = m , refl
 
+data Even : ℕ → Set where
+  ev0 : Even zero
+  ev2 : ∀ {n} → Even n → Even (suc (suc n))
+
+ev-ex : ∀ {n : ℕ} → Even n → ∃[ m ] (2 * m ≡ n)
+ev-ex ev0 =  (zero , refl)
+ev-ex (ev2 ev) with ev-ex ev
+... | (m , refl) = (suc m , lemma m)
+