From 652da6c516f979094719515bb3e414d38e28b919 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Wed, 14 Feb 2018 19:34:10 -0200
Subject: [PATCH] Lists, added All and Any
---
README.md | 1 -
src/Isomorphism.lagda | 2 +-
src/Lists.lagda | 160 ++++++++++++++++++++++++++++++++++++++----
src/Logic.lagda | 22 ++++--
src/extra/Dummy.agda | 2 +
5 files changed, 167 insertions(+), 20 deletions(-)
diff --git a/README.md b/README.md
index 23c3de94..9c04b1ad 100644
--- a/README.md
+++ b/README.md
@@ -52,7 +52,6 @@ https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
C-c C-c x split on variable x
C-c C-space fill in hole
-
Also see [here](
http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
).
diff --git a/src/Isomorphism.lagda b/src/Isomorphism.lagda
index b64b4c76..71ee037c 100644
--- a/src/Isomorphism.lagda
+++ b/src/Isomorphism.lagda
@@ -27,7 +27,7 @@ record _≃_ (A B : Set) : Set where
fro : B → A
invˡ : ∀ (x : A) → fro (to x) ≡ x
invʳ : ∀ (y : B) → to (fro y) ≡ y
-open _≃_
+open _≃_
\end{code}
Let's unpack the definition. An isomorphism between sets `A` and `B` consists
of four things:
diff --git a/src/Lists.lagda b/src/Lists.lagda
index 0ed92380..822cc470 100644
--- a/src/Lists.lagda
+++ b/src/Lists.lagda
@@ -13,8 +13,12 @@ introducing polymorphic types and functions.
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 using (ℕ; zero; suc; _+_; _*_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
+open import Relation.Nullary using (¬_)
+open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+open import Isomorphism using (_≃_)
+open import Function using (_∘′_)
\end{code}
## Lists
@@ -601,7 +605,12 @@ Use fold to define a function to find the product of a list of numbers.
Show that fold and append are related as follows.
+\begin{code}
+postulate
+ foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
+\end{code}
+
*Exercise* (`map-is-foldr`) <!-- `mapIsFold` in Data.List.Properties -->
@@ -660,9 +669,9 @@ list, are all examples of monoids.
If `_⊕_` and `e` form a monoid, then we can re-express fold on the
same operator and an arbitrary value.
\begin{code}
-fold-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → Monoid _⊗_ e →
- ∀ (y : A) (xs : List A) → foldr _⊗_ e xs ⊗ y ≡ foldr _⊗_ y xs
-fold-monoid _⊗_ e ⊗-monoid y [] =
+foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → Monoid _⊗_ e →
+ ∀ (xs : List A) (y : A) → foldr _⊗_ e xs ⊗ y ≡ foldr _⊗_ y xs
+foldr-monoid _⊗_ e ⊗-monoid [] y =
begin
foldr _⊗_ e [] ⊗ y
≡⟨⟩
@@ -672,35 +681,158 @@ fold-monoid _⊗_ e ⊗-monoid y [] =
≡⟨⟩
foldr _⊗_ y []
∎
-fold-monoid _⊗_ e ⊗-monoid y (x ∷ xs) =
+foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
begin
foldr _⊗_ e (x ∷ xs) ⊗ y
≡⟨⟩
(x ⊗ foldr _⊗_ e xs) ⊗ y
≡⟨ assoc ⊗-monoid x (foldr _⊗_ e xs) y ⟩
x ⊗ (foldr _⊗_ e xs ⊗ y)
- ≡⟨ cong (x ⊗_) (fold-monoid _⊗_ e ⊗-monoid y xs) ⟩
+ ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e ⊗-monoid xs y) ⟩
x ⊗ (foldr _⊗_ y xs)
≡⟨⟩
foldr _⊗_ y (x ∷ xs)
∎
\end{code}
-As a consequence of `foldr-++` and `fold-monoid`, it is easy to show
+As a consequence, using a previous exercise, we have the following.
+\begin{code}
+foldr-monoid-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → Monoid _⊗_ e →
+ (xs ys : List A) → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
+foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
+ begin
+ foldr _⊗_ e (xs ++ ys)
+ ≡⟨ foldr-++ _⊗_ e xs ys ⟩
+ foldr _⊗_ (foldr _⊗_ e ys) xs
+ ≡⟨ sym (foldr-monoid _⊗_ e monoid-⊗ xs (foldr _⊗_ e ys)) ⟩
+ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
+ ∎
+\end{code}
+
+## All and Any
- foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
+We can also define predicates over lists. Two of the most important are `All` and `Any`.
+Predicate `All P` holds if predicate `P` is satisfied by every element of a list.
+\begin{code}
+data All {A : Set} (P : A → Set) : List A → Set where
+ [] : All P []
+ _∷_ : {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)
+\end{code}
+The type has two constructors, reusing the names of the same constructors for lists.
+The first asserts that `All P` always holds of the empty list.
+The second asserts that if `P` holds of the head of a list, and if `All P`
+holds of the tail of the list, then `All P` holds for the entire list.
+Agda uses type information to distinguish whether the constructor is building
+a list, or evidence that `All P` holds.
-## Element
+For example, `All (_≤ 2)` holds of a list where every element is less
+than or equal to two. Recall that `z≤n` proves `zero ≤ n` for any
+`n`, and that if `m≤n` proves `m ≤ n` then `s≤s m≤n` proves `suc m ≤
+suc n`, for any `m` and `n`.
+\begin{code}
+ex₁₀ : All (_≤ 2) ([ 0 , 1 , 2 ])
+ex₁₀ = z≤n ∷ (s≤s z≤n) ∷ (s≤s (s≤s z≤n)) ∷ []
+\end{code}
+Here `_∷_` and `[]` are the constructors of `All P` rather than of `List A`.
+The three items are proofs of `0 ≤ 2`, `1 ≤ 2`, and `2 ≤ 2`, respectively.
+
+Predicate `Any P` holds if predicate `P` is satisfied by some element of a list.
+\begin{code}
+data Any {A : Set} (P : A → Set) : List A → Set where
+ here : {x : A} {xs : List A} → P x → Any P (x ∷ xs)
+ there : {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)
+\end{code}
+The first constructor provides evidence that the head of the list satisfies `P`,
+while the second provides evidence that the tail of the list satisfies `Any P`.
+For example, we can define list membership as follows.
+\begin{code}
+infix 4 _∈_
+
+_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
+x ∈ xs = Any (x ≡_) xs
+
+_∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set
+x ∉ xs = ¬ (x ∈ xs)
+\end{code}
+For example, we have `0 ∈ ([ 0 , 1 , 0 ])`. Indeed, we can demonstrate
+this fact in two different ways, corresponding to the two different
+occurrences of zero in the list, as the first element and as the third element.
+\begin{code}
+ex₁₁ ex₁₂ : 0 ∈ ([ 0 , 1 , 0 ])
+ex₁₁ = here refl
+ex₁₂ = there (there (here refl))
+\end{code}
+Further, we can demonstrate that two is not in the list, because
+any possible proof that it is in the list leads to contradiction.
+\begin{code}
+ex₁₃ : 2 ∉ ([ 0 , 1 , 0 ])
+ex₁₃ (here ())
+ex₁₃ (there (here ()))
+ex₁₃ (there (there (here ())))
+ex₁₃ (there (there (there ())))
+\end{code}
+The four occurrences of `()` attest to the fact that there is no
+possible evidence for the facts `2 ≡ 0`, `2 ≡ 1`, `2 ≡ 0`, and
+`2 ∈ []`, respectively.
+
+A predicate holds for every element of one list appended to another if and
+only if it holds for every element of each list. Indeed, an even stronger
+result is true, as we can show that the two types are isomorphic.
+\begin{code}
+All-++ : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) ≃ (All P xs × All P ys)
+All-++ xs ys =
+ record
+ { to = to xs ys
+ ; fro = fro xs ys
+ ; invˡ = invˡ xs ys
+ ; invʳ = invʳ xs ys
+ }
+
+ where
+
+ to : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) → (All P xs × All P ys)
+ to [] ys AllPys = ⟨ [] , AllPys ⟩
+ to (x ∷ xs) ys (Px ∷ AllPxsys) with to xs ys AllPxsys
+ ... | ⟨ AllPxs , AllPys ⟩ = ⟨ Px ∷ AllPxs , AllPys ⟩
+
+ fro : ∀ { A : Set} {P : A → Set} (xs ys : List A) → All P xs × All P ys → All P (xs ++ ys)
+ fro [] ys ⟨ [] , AllPys ⟩ = AllPys
+ fro (x ∷ xs) ys ⟨ Px ∷ AllPxs , AllPys ⟩ = Px ∷ fro xs ys ⟨ AllPxs , AllPys ⟩
+
+ invˡ : ∀ { A : Set} {P : A → Set} (xs ys : List A) → (AllPxsys : All P (xs ++ ys)) →
+ fro xs ys (to xs ys AllPxsys) ≡ AllPxsys
+ invˡ [] ys AllPys = refl
+ invˡ (x ∷ xs) ys (Px ∷ AllPxsys) = cong (Px ∷_) (invˡ xs ys AllPxsys)
+
+ invʳ : ∀ { A : Set} {P : A → Set} (xs ys : List A) → (AllPxsAllPys : All P xs × All P ys) →
+ to xs ys (fro xs ys AllPxsAllPys) ≡ AllPxsAllPys
+ invʳ [] ys ⟨ [] , AllPys ⟩ = refl
+ invʳ (x ∷ xs) ys ⟨ Px ∷ AllPxs , AllPys ⟩ rewrite invʳ xs ys ⟨ AllPxs , AllPys ⟩ = refl
+\end{code}
+
+*Exercise* `Any-++`
+
+Prove a result similar to `All-++`, but with `Any` in place of `All`, and a suitable
+replacement for `_×_`. As a consequence, demonstrate an isomorphism relating
+`_∈_` and `_++_`.
+
+*Exercise* `¬Any≃All¬`
+
+Show that `Any` and `All` satisfy a version of De Morgan's Law.
\begin{code}
-data _∈_ {A : Set} (x : A) : List A → Set where
- here : {y : A} {ys : List A} → x ≡ y → x ∈ y ∷ ys
- there : {y : A} {ys : List A} → x ∈ ys → x ∈ y ∷ ys
-
-infix 4 _∈_
+postulate
+ ¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A) → ¬ Any P xs ≃ All (λ x → ¬ P x) xs
\end{code}
+Do we also have the following?
+
+ ¬ All P xs ≃ Any (λ x → ¬ P x) xs
+
+If so, prove; if not, explain why.
+
+
## Unicode
∷ U+2237 PROPORTION (\::)
diff --git a/src/Logic.lagda b/src/Logic.lagda
index 21bc32bb..15650026 100644
--- a/src/Logic.lagda
+++ b/src/Logic.lagda
@@ -833,6 +833,22 @@ excluded-middle-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
excluded-middle-irrefutable k = k (inj₂ (λ a → k (inj₁ a)))
\end{code}
+*Exercise* (`¬⊎≃׬`)
+
+Show that conjunction, disjunction, and negation are related by a
+version of De Morgan's Law.
+\begin{code}
+postulate
+ ¬⊎≃׬ : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
+\end{code}
+This result is an easy consequence of something we've proved previously.
+
+Do we also have the following?
+
+ ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
+
+If so, prove; if not, explain why.
+
## Intuitive and Classical logic
@@ -878,7 +894,7 @@ a disjoint sum.
(The passage above is taken from "Propositions as Types", Philip Wadler,
*Communications of the ACM*, December 2015.)
-**Exercise** Prove the following six formulas are equivalent.
+**Exercise** Prove the following five formulas are equivalent.
\begin{code}
lone ltwo : Level
@@ -890,9 +906,7 @@ ltwo = lsuc lone
excluded-middle = ∀ {A : Set} → A ⊎ ¬ A
peirce = ∀ {A B : Set} → (((A → B) → A) → A)
implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
-de-morgan = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
-de-morgan′ = ∀ {A B : Set} → ¬ (¬ A ⊎ ¬ B) → A × B
-
+de-morgan = ∀ {A B : Set} → ¬ (A × B) → ¬ A ⊎ ¬ B
\end{code}
It turns out that an assertion such as `Set : Set` is paradoxical.
diff --git a/src/extra/Dummy.agda b/src/extra/Dummy.agda
index 1f9c88b6..8483a60d 100644
--- a/src/extra/Dummy.agda
+++ b/src/extra/Dummy.agda
@@ -1,4 +1,6 @@
import Data.List.Properties
+import Data.List.All
import Data.Nat.Properties
import Data.Nat.Properties.Simple
+import Relation.Nullary