halfway through Quantifiers

index.md

@@ -26,7 +26,7 @@ material in a different way; see the [Preface](Preface).
   - [Equality: Equality and equational reasoning](Equality)
   - [Isomorphism: Isomorphism and embedding](Isomorphism)
   - [Connectives: Conjunction, Disjunction, and Implication](Connectives)
-  - [Negation: Negation, with Classical and Intuitionistic Logic](Negation)
+  - [Negation: Negation, with Intuitionistic and Classical Logic](Negation)
   - [Quantiers: Universals and Existentials](Quantifiers)
   - [Lists: Lists and other data types](Lists)
   - [Decidable: Booleans and decision procedures](Decidable)

src/Connectives.lagda

@@ -534,7 +534,6 @@ Right identity follows from commutativity of sum and left identity.
   ≃-∎
 \end{code}
 
-
 ## Implication is function
 
 Given two propositions `A` and `B`, the implication `A → B` holds if
@@ -543,9 +542,9 @@ the function type, which has appeared throughout this book.
 
 Evidence that `A → B` holds is of the form
 
-    λ{ x → N }
+    λ (x : A) → N x
 
-where `N` is a term of type `B` containing as a free variable `x` of type `A`.
+where `N x` is a term of type `B` containing as a free variable `x` of type `A`.
 Given a term `L` providing evidence that `A → B` holds, and a term `M`
 providing evidence that `A` holds, the term `L M` provides evidence that
 `B` holds.  In other words, evidence that `A → B` holds is a function that
@@ -555,7 +554,7 @@ Put another way, if we know that `A → B` and `A` both hold,
 then we may conclude that `B` holds.
 \begin{code}
 →-elim : ∀ {A B : Set} → (A → B) → A → B
-→-elim f x = f x
+→-elim L M = L M
 \end{code}
 In medieval times, this rule was known by the name *modus ponens*.
 It corresponds to function application.
@@ -566,10 +565,10 @@ while applying a function is referred to as *eliminating* the function.
 
 Elimination followed by introduction is the identity.
 \begin{code}
-η-→ : ∀ {A B : Set} (f : A → B) → (λ{x → f x}) ≡ f
+η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
 η-→ {A} {B} f = extensionality η-helper
   where
-  η-helper : (x : A) → (λ (x′ : A) → f x′) x ≡ f x
+  η-helper : (x : A) → (λ (x : A) → f x) x ≡ f x
   η-helper x = refl
 \end{code}
 The proof depends on extensionality.
@@ -672,8 +671,8 @@ That is, the assertion that if either `A` holds or `B` holds then `C` holds
 is the same as the assertion that if `A` holds then `C` holds and if
 `B` holds then `C` holds.  The proof of the left inverse requires extensionality.
 \begin{code}
-→-distributes-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
+→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
-→-distributes-⊎ =
+→-distrib-⊎ =
   record
     { to      = λ{ f → ( (λ{ x → f (inj₁ x) }) , (λ{ y → f (inj₂ y) }) ) }
     ; from    = λ{ (g , h) → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
@@ -695,8 +694,8 @@ 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}
-→-distributes-× : ∀ {A B C : Set} → (A → B × C) ≃ ((A → B) × (A → C))
+→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ ((A → B) × (A → C))
-→-distributes-× =
+→-distrib-× =
   record
     { to      = λ{ f → ( (λ{ x → proj₁ (f x) }) , (λ{ y → proj₂ (f y)}) ) }
     ; from    = λ{ (g , h) → λ{ x → (g x , h x) } }
@@ -711,8 +710,8 @@ 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}
-×-distributes-⊎ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
+×-distrib-⊎ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
-×-distributes-⊎ =
+×-distrib-⊎ =
   record
     { to   = λ { ((inj₁ x) , z) → (inj₁ (x , z)) 
                ; ((inj₂ y) , z) → (inj₂ (y , z))
@@ -731,8 +730,8 @@ 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}
-⊎-distributes-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≲ ((A ⊎ C) × (B ⊎ C))
+⊎-distrib-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≲ ((A ⊎ C) × (B ⊎ C))
-⊎-distributes-× =
+⊎-distrib-× =
   record
     { to   = λ { (inj₁ (x , y)) → (inj₁ x , inj₁ y)
                ; (inj₂ z)       → (inj₂ z , inj₂ z)
@@ -800,6 +799,7 @@ This chapter uses the following unicode.
     ⊎  U+228E  MULTISET UNION (\u+)
     ⊤  U+22A4  DOWN TACK (\top)
     ⊥  U+22A5  UP TACK (\bot)
+    η  U+03B7  GREEK SMALL LETTER ETA (\eta)
     ₁  U+2081  SUBSCRIPT ONE (\_1)
     ₂  U+2082  SUBSCRIPT TWO (\_2)
     ⇔  U+21D4  LEFT RIGHT DOUBLE ARROW (\<=>)

src/Equality.lagda

@@ -59,8 +59,9 @@ but on the left-hand side of the equation the argument has been instantiated to
 which requires that `x` and `y` are the same.  Hence, for the right-hand side of the equation
 we need a term of type `x ≡ x`, and `refl` will do.
 
-It is instructive to develop `sym` interactively.
+It is instructive to develop `sym` interactively.  To start, we supply
-To start, we supply a variable for the argument on the left, and a hole for the body on the right:
+a variable for the argument on the left, and a hole for the body on
+the right:
 
     sym : ∀ {ℓ} {A : Set ℓ} {x y : A} →  x ≡ y → y ≡ x
     sym e = {! !}
@@ -75,8 +76,9 @@ If we go into the hole and type `C-C C-,` then Agda reports:
     .A : Set .ℓ
     .ℓ : .Agda.Primitive.Level
 
-If in the hole we type `C-C C-C e` then Agda will instantiate `e` to all possible constructors,
+If in the hole we type `C-C C-C e` then Agda will instantiate `e` to
-with one equation for each. There is only one possible constructor:
+all possible constructors, with one equation for each. There is only
+one possible constructor:
 
     sym : ∀ {ℓ} {A : Set ℓ} {x y : A} →  x ≡ y → y ≡ x
     sym refl = {! !}

src/Negation.lagda

@@ -1,19 +1,16 @@
 ---
-title     : "Negation: Negation, with Classical and Intuitionistic Logic"
+title     : "Negation: Negation, with Intuitionistic and Classical Logic"
 layout    : page
 permalink : /Negation
 ---
 
+This chapter introduces negation, and discusses intuitionistic
+and classical logic.
+
 ## Imports
 
 \begin{code}
-import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_; refl; sym; trans; cong)
-open Eq.≡-Reasoning
 open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
-open Isomorphism.≃-Reasoning
-open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
-open import Data.Nat.Properties.Simple using (+-suc)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
@@ -84,11 +81,11 @@ can conclude `¬ ¬ A` (evidenced by `¬¬-intro x`).  Then from
 `¬ ¬ ¬ A` and `¬ ¬ A` we have a contradiction (evidenced by
 `¬¬¬x (¬¬-intro x)`.  Hence we have shown `¬ A`.
 
-Another law of logic is the *contrapositive*,
+Another law of logic is *contraposition*,
 stating that if `A` implies `B`, then `¬ B` implies `¬ A`.
 \begin{code}
-contrapositive : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
+contraposition : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
-contrapositive f ¬y x = ¬y (f x)
+contraposition f ¬y x = ¬y (f x)
 \end{code}
 Let `f` be evidence of `A → B` and let `¬y` be evidence of `¬ B`.  We
 will show that assuming `A` leads to a contradiction, and hence
@@ -268,7 +265,7 @@ Philip Wadler, *International Conference on Functional Programming*, 2003.)
 
 ### Exercise
 
-Prove the following four formulas are equivalent to each other,
+Prove the following three formulas are equivalent to each other,
 and to the formulas `EM` and `⊎-Dual-+` given earlier.
 \begin{code}
 ¬¬-Elim Peirce Implication : Set₁
@@ -277,61 +274,34 @@ Peirce = ∀ {A B : Set} → (((A → B) → A) → A)
 Implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
 \end{code}
 
-<!-- 
     
-It turns out that an assertion such as `Set : Set` is paradoxical.
+### Exercise (`¬-stable`, `×-stable`)
-Therefore, there are an infinite number of different levels of sets,
-where `Set lzero : Set lone` and `Set lone : Set ltwo`, and so on,
-where `lone` is `lsuc lzero`, and `ltwo` is `lsuc lone`, analogous to
-the way we represent the natural nuambers. So far, we have only used
-the type `Set`,  which is equivalent to `Set lzero`.  Here, since each
-of `double-negation` and the others defines a type, we need to use
-`Set₁` as the "type of types".
-
--->
-
-[NOTES]
-
-Two halves of de Morgan's laws hold intuitionistically.  The other two
-halves are each equivalent to the law of double negation.
 
+Say that a formula is *stable* if double negation elimination holds for it.
 \begin{code}
-dem1 : ∀ {A B : Set} → A × B → ¬ (¬ A ⊎ ¬ B)
+Stable : Set → Set
-dem1 (a , b) (inj₁ ¬a) = ¬a a
+Stable A = ¬ ¬ A → A
-dem1 (a , b) (inj₂ ¬b) = ¬b b
+\end{code}
+Show that any negated formula is stable, and that the conjunction
+of two stable formulas is stable.
+\begin{code}
+¬-Stable : Set₁
+¬-Stable = ∀ {A : Set} → Stable (¬ A)
 
-dem2 : ∀ {A B : Set} → A ⊎ B → ¬ (¬ A × ¬ B)
+×-Stable : Set₁
-dem2 (inj₁ a) (¬a , ¬b) = ¬a a
+×-Stable = ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
-dem2 (inj₂ b) (¬a , ¬b) = ¬b b
 \end{code}
 
-For the other variant of De Morgan's law, one way is an isomorphism.
+## Standard Prelude
+
+Definitions similar to those in this chapter can be found in the standard library.
 \begin{code}
--- dem-≃ : ∀ {A B : Set} → (¬ (A ⊎ B)) ≃ (¬ A × ¬ B)
+import Relation.Nullary using (¬_)
--- dem-≃ = →-distributes-⊎
+import Relation.Nullary.Negation using (contraposition)
 \end{code}
 
-The other holds in only one direction.
+## Unicode
-\begin{code}
-dem-half : ∀ {A B : Set} → ¬ A ⊎ ¬ B → ¬ (A × B)
-dem-half (inj₁ ¬a) (a , b) = ¬a a
-dem-half (inj₂ ¬b) (a , b) = ¬b b
-\end{code}
-
-The other variant does not appear to be equivalent to classical logic.
-So that undermines my idea that basic propositions are either true
-intuitionistically or equivalent to classical logic.
-
-For several of the laws equivalent to classical logic, the reverse
-direction holds in intuitionistic long.
-\begin{code}
-implication-inv : ∀ {A B : Set} → (¬ A ⊎ B) → A → B
-implication-inv (inj₁ ¬a) a = ⊥-elim (¬a a)
-implication-inv (inj₂ b)  a = b
-
-demorgan-inv : ∀ {A B : Set} → A ⊎ B → ¬ (¬ A × ¬ B)
-demorgan-inv (inj₁ a) (¬a , ¬b) =  ¬a a
-demorgan-inv (inj₂ b) (¬a , ¬b) =  ¬b b
-\end{code}
 
+This chapter uses the following unicode.
 
+    ¬  U+00AC  NOT SIGN (\neg)

src/Quantifiers.lagda

@@ -4,6 +4,8 @@ layout    : page
 permalink : /Quantifiers
 ---
 
+This chapter introduces universal and existential quatification.
+
 ## Imports
 
 \begin{code}
@@ -16,6 +18,8 @@ open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Nat.Properties.Simple using (+-suc)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
 \end{code}
 
 In what follows, we will occasionally require [extensionality][extensionality].
@@ -29,52 +33,73 @@ postulate
 
 ## Universals
 
-Given a variable `x` of type `A` and a proposition `B[x]` which
+Given a variable `x` of type `A` and a proposition `B x` which
 contains `x` as a free variable, the universally quantified
-proposition `∀ (x : A) → B[x]` holds if for every term `M` of type
+proposition `∀ (x : A) → B x` holds if for every term `M` of type
-`A` the proposition `B[M]` holds.  Here `B[M]` stands for
+`A` the proposition `B M` holds.  Here `B M` stands for
-the proposition `B[x]` with each free occurrence of `x` replaced by
+the proposition `B x` with each free occurrence of `x` replaced by
-`M`.  The variable `x` appears free in `B[x]` but bound in
+`M`.  The variable `x` appears free in `B x` but bound in
-`∀ (x : A) → B[x]`.  We formalise universal quantification using the
+`∀ (x : A) → B x`.  We formalise universal quantification using the
 dependent function type, which has appeared throughout this book.
 
-Evidence that `∀ (x : A) → B[x]` holds is of the form
+Evidence that `∀ (x : A) → B x` holds is of the form
 
-    λ (x : A) → N[x]
+    λ (x : A) → N x
 
-where `N[x]` is a term of type `B[x]`; here `N[x]` is a term and `B[x]`
+where `N x` is a term of type `B x`, and `N x` and `B x` both contain
-is a proposition (or type) both containing as a free variable `x` of
+a free variable `x` of type `A`.  Given a term `L` providing evidence
-type `A`.  Given a term `L` providing evidence that `∀ (x : A) → B[x]`
+that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L
-holds and a term `M` of type `A`, the term `L M` provides evidence
+M` provides evidence that `B M` holds.  In other words, evidence that
-that `B[M]` holds.  In other words, evidence that `∀ (x : A) → B[x]`
+`∀ (x : A) → B x` holds is a function that converts a term `M` of type
-holds is a function that converts a term `M` of type `A` into evidence
+`A` into evidence that `B M` holds.
-that `B[M]` holds.
 
-Put another way, if we know that `∀ (x : A) → B[x]` holds and that `M`
+Put another way, if we know that `∀ (x : A) → B x` holds and that `M`
-is a term of type `A` then we may conclude that `B[M]` holds. In
+is a term of type `A` then we may conclude that `B M` holds.
-medieval times, this rule was known by the name *dictum de omni*.
+\begin{code}
+∀-elim : ∀ {A : Set} {B : A → Set} → (∀ (x : A) → B x) → (M : A) → B M
+∀-elim L M = L M
+\end{code}
+In medieval times, this rule was known by the name *dictum de omni*.
 
-If we introduce a universal and the immediately eliminate it, we can
+Ordinary function types arise as the special case of dependent
-always simplify the resulting term. Thus
+function types where the range does not depend on a variable drawn
-
+from the domain.  When an ordinary function is viewed as evidence of
-    (λ (x : A) → N[x]) M
+implication, both its domain and range are viewed as types of
-
+evidence, whereas when a dependent function is viewed as evidence of a
-simplifies to `N[M]` of type `B[M]`, where `N[M]` stands for the term
+universal, its domain is viewed as a data type and its range is viewed
-`N[x]` with each free occurrence of `x` replaced by `M` of type `A`.
+as a type of evidence.  This is just a matter of interpretation, since
+in Agda data types and types of evidence are indistinguishable.
 
 Unlike with conjunction, disjunction, and implication, there is no simple
 analogy between universals and arithmetic.
 
+### Exercise (`∀-distrib-×`)
+
+Show that universals distribute over conjunction.
+\begin{code}
+∀-Distrib-× = ∀ {A : Set} {B C : A → Set} →
+  (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
+\end{code}
+Compare this with the result (`→-distrib-×`) in Chapter [Connectives](Connectives).
+
+### Exercise (`⊎∀-implies-∀⊎`)
+
+Show that a disjunction of universals implies a universal of disjunctions.
+\begin{code}
+⊎∀-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.
 
 ## Existentials
 
-Given a variable `x` of type `A` and a proposition `B[x]` which
+Given a variable `x` of type `A` and a proposition `B x` which
 contains `x` as a free variable, the existentially quantified
-proposition `∃ (λ (x : A) → B[x])` holds if for some term `M` of type
+proposition `∃[ x ] → B x` holds if for some term `M` of type
-`A` the proposition `B[M]` holds.  Here `B[M]` stands for
+`A` the proposition `B M` holds.  Here `B M` stands for
-the proposition `B[x]` with each free occurrence of `x` replaced by
+the proposition `B x` with each free occurrence of `x` replaced by
-`M`.  The variable `x` appears free in `B[x]` but bound in
+`M`.  The variable `x` appears free in `B x` but bound in
-`∃ (λ (x : A) → B[x])`.
+`∃[ x ] → B x`.
 
 It is common to adopt a notation such as `∃[ x : A ]→ B[x]`,
 which introduces `x` as a bound variable of type `A` that appears
@@ -85,18 +110,23 @@ to introduce `x` as a bound variable.
 We formalise existential quantification by declaring a suitable
 inductive type.
 \begin{code}
-data ∃ {A : Set} (B : A → Set) : Set where
+data ∃ (A : Set) (B : A → Set) : Set where
-  _,_ : (x : A) → B x → ∃ B
+  _,_ : (x : A) → B x → ∃ A B
 \end{code}
 Evidence that `∃ (λ (x : A) → B[x])` holds is of the form
 `(M , N)` where `M` is a term of type `A`, and `N` is evidence
 that `B[M]` holds.
 
+\begin{code}
+syntax ∃ A (λ x → B) = ∃[ x ∈ A ] B
+\end{code}
+
 Given evidence that `∃ (λ (x : A) → B[x])` holds, and
 given evidence that `∀ (x : A) → B[x] → C` holds, where `C` does
 not contain `x` as a free variable, we may conclude that `C` holds.
 \begin{code}
-∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → ∃ B → (∀ (x : A) → B x → C) → C
+∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} →
+  (∃[ x ∈ A ] B x) → (∀ (x : A) → B x → C) → C
 ∃-elim (M , N) P = P M N
 \end{code}
 In other words, if we know for every `x` of type `A` that `B[x]`
@@ -148,7 +178,7 @@ 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)
+ev-ex : ∀ {n : ℕ} → even n → ∃[ m ∈ ℕ ] (2 * m ≡ n)
 ev-ex ev0 =  (zero , refl)
 ev-ex (ev+2 ev) with ev-ex ev
 ... | (m , refl) = (suc m , lemma m)
@@ -171,7 +201,7 @@ return a pair consisting of `suc m` and a proof that `2 * suc m ≡ suc
 
 Here is the proof in the reverse direction.
 \begin{code}
-ex-ev : ∀ {n : ℕ} → ∃(λ (m : ℕ) → 2 * m ≡ n) → even n
+ex-ev : ∀ {n : ℕ} → ∃[ m ∈ ℕ ] (2 * m ≡ n) → even n
 ex-ev (zero , refl) = ev0
 ex-ev (suc m , refl) rewrite lemma m = ev+2 (ex-ev (m , refl))
 \end{code}
@@ -196,11 +226,11 @@ 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 ∈ A ] B x) ≃ ∀ (x : A) → ¬ B x
 ¬∃∀ =
   record
-    { to   =  λ { ¬∃bx x bx → ¬∃bx (x , bx) }
+    { to      =  λ { ¬∃bx x bx → ¬∃bx (x , bx) }
-    ; from  =  λ { ∀¬bx (x , bx) → ∀¬bx x bx }
+    ; from    =  λ { ∀¬bx (x , bx) → ∀¬bx x bx }
     ; from∘to =  λ { ¬∃bx → extensionality (λ { (x , bx) → refl }) } 
     ; to∘from =  λ { ∀¬bx → refl } 
     }
@@ -223,7 +253,12 @@ requires extensionality.
 
 *Exercise* Show `∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x)`.
 
+## Standard Prelude
 
+Definitions similar to those in this chapter can be found in the standard library.
+\begin{code}
+import Data.Product using (∃)
+\end{code}
 
 ## Unicode