From a61fdc87ff83bef83229989dc12d398612aeb52f Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Mon, 3 Sep 2018 14:27:38 +0100 Subject: [PATCH] negation exercises --- extra/answers/NegationAns.lagda | 73 ++++++++++++++++++++++++++------- src/plfa/Connectives.lagda | 4 +- src/plfa/Negation.lagda | 56 +++++++++---------------- 3 files changed, 80 insertions(+), 53 deletions(-) diff --git a/extra/answers/NegationAns.lagda b/extra/answers/NegationAns.lagda index a949d552..450c7715 100644 --- a/extra/answers/NegationAns.lagda +++ b/extra/answers/NegationAns.lagda @@ -9,10 +9,11 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) open import Data.Unit using (⊤; tt) open import Data.Empty using (⊥; ⊥-elim) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Data.Product using (_×_; _,_; proj₁; proj₂) -open import Isomorphism using (_≃_) -open import Negation using - (¬_; id; EM; em-irrefutable; ¬¬-Elim; Peirce; Implication; ×-Implies-⊎) +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) +open import Relation.Nullary using (¬_) +-- open import Isomorphism using (_≃_) +-- open import Negation using +-- (¬_; id; EM; em-irrefutable; ¬¬-Elim; Peirce; Implication; ×-Implies-⊎) \end{code} In what follows, we occasionally require [extensionality][extensionality]. @@ -28,25 +29,66 @@ postulate *Equivalences for classical logic* \begin{code} -ex1 : ¬¬-Elim → EM -ex1 h = h em-irrefutable +em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A) +em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) }) -ex2 : EM → Implication -ex2 em f with em +EM : Set₁ +EM = ∀ {A : Set} → A ⊎ ¬ A + +¬¬-Elim : Set₁ +¬¬-Elim = ∀ {A : Set} → ¬ ¬ A → A + +Implication : Set₁ +Implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B + +Peirce : Set₁ +Peirce = ∀ {A B : Set} → ((A → B) → A) → A + +DeMorgan : Set₁ +DeMorgan = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B + +ex1 : ¬¬-Elim → EM +ex1 ¬¬-elim = ¬¬-elim em-irrefutable + +ex2 : EM → ¬¬-Elim +ex2 em ¬¬a with em +... | inj₁ a = a +... | inj₂ ¬a = ⊥-elim (¬¬a ¬a) + +ex3 : EM → Implication +ex3 em f with em ... | inj₁ a = inj₂ (f a) ... | inj₂ ¬a = inj₁ ¬a -ex3 : EM → Peirce -ex3 em k with em +ex4 : Implication → EM +ex4 imp = swap (imp (λ a → a)) + where + swap : ∀ {A B} → A ⊎ B → B ⊎ A + swap (inj₁ a) = inj₂ a + swap (inj₂ b) = inj₁ b + +ex5 : EM → Peirce +ex5 em k with em ... | inj₁ a = a ... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a)) -ex4 : EM → ×-Implies-⊎ -ex4 em ¬a×b with em | em -... | inj₁ a | inj₁ b = ⊥-elim (¬a×b (a , b)) -... | inj₁ a | inj₂ ¬b = inj₂ ¬b -... | inj₂ ¬a | _ = inj₁ ¬a +ex6 : Peirce → EM +ex6 peirce = peirce (λ ¬em → ⊥-elim (em-irrefutable ¬em)) +ex7 : EM → DeMorgan +ex7 em ¬[¬a׬b] with em | em +... | inj₁ a | _ = inj₁ a +... | inj₂ ¬a | inj₁ b = inj₂ b +... | inj₂ ¬a | inj₂ ¬b = ⊥-elim (¬[¬a׬b] ⟨ ¬a , ¬b ⟩) + +ex8 : DeMorgan → EM +ex8 deMorgan {A} = deMorgan ¬[¬a׬¬a] + where + ¬[¬a׬¬a] : ¬ (¬ A × ¬ ¬ A) + ¬[¬a׬¬a] ⟨ ¬a , ¬¬a ⟩ = ¬¬a ¬a + + +{- ⊤⊥-iso : (¬ ⊥) ≃ ⊤ ⊤⊥-iso = record @@ -55,6 +97,7 @@ ex4 em ¬a×b with em | em ; from∘to = λ{ _ → extensionality (λ ()) } ; to∘from = λ{ tt → refl } } +-} \end{code} *Existentials and Universals* diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda index 7418e32b..5a59ef25 100644 --- a/src/plfa/Connectives.lagda +++ b/src/plfa/Connectives.lagda @@ -799,7 +799,7 @@ This is called a _weak distributive law_. Give the corresponding distributive law, and explain how it relates to the weak version. -#### Exercise (`⊎×-implies-×⊎`) +#### Exercise `⊎×-implies-×⊎` Show that a disjunct of conjuncts implies a conjunct of disjuncts. \begin{code} @@ -809,7 +809,7 @@ postulate Does the converse hold? If so, prove; if not, give a counterexample. -#### Exercise (`_⇔_`) {#iff} +#### Exercise `_⇔_` {#iff} Define equivalence of propositions (also known as "if and only if") as follows. \begin{code} diff --git a/src/plfa/Negation.lagda b/src/plfa/Negation.lagda index 1f1687b0..f991990f 100644 --- a/src/plfa/Negation.lagda +++ b/src/plfa/Negation.lagda @@ -156,14 +156,14 @@ the other. -### Exercise (`≢`, `<-irrerflexive`) +### Exercise `<-irrerflexive` Using negation, show that [strict inequality]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#strict-inequality) is irreflexive, that is, `n < n` holds for no `n`. -### Exercise (`trichotomy`) +### Exercise `trichotomy` Show that strict inequality satisfies [trichotomy]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#trichotomy), @@ -177,21 +177,19 @@ Here "exactly one" means that one of the three must hold, and each implies the negation of the other two. -### Exercise (`⊎-dual-×`) +### Exercise `⊎-dual-×` Show that conjunction, disjunction, and negation are related by a version of De Morgan's Law. -\begin{code} -postulate - ⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B) -\end{code} + + ¬ (A ⊎ B) ≃ (¬ A) × (¬ B) + This result is an easy consequence of something we've proved previously. Is there also a term of the following type? -\begin{code} -postulate - ×-dual-⊎ : ∀ {A B : Set} → ¬ (A × B) ≃ (¬ A) ⊎ (¬ B) -\end{code} + + ¬ (A × B) ≃ (¬ A) ⊎ (¬ B) + If so, prove; if not, explain why. @@ -327,21 +325,20 @@ just handed to him. Philip Wadler, _International Conference on Functional Programming_, 2003.) -#### Exercise +#### Exercise `classical` (stretch) -Consider the following five terms of the given types. -\begin{code} -postulate - em′ : ∀ {A : Set} → A ⊎ ¬ A - ¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A - peirce : ∀ {A B : Set} → (((A → B) → A) → A) - →-implies-⊎ : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B - ×-implies-⊎ : ∀ {A B : Set} → ¬ (A × B) → (¬ A) ⊎ (¬ B) -\end{code} -Show that given any one term of the specified type, we can derive the others. +Consider the following principles. + + * Excluded Middle: `A ⊎ ¬ A`, for all `A` + * Double Negation Elimination: `¬ ¬ A → A`, for all `A` + * Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`. + * Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`. + * De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`. + +Show that each of these implies all the others. -### Exercise (`¬-stable`, `×-stable`) +#### Exercise `stable` (stretch) Say that a formula is _stable_ if double negation elimination holds for it. \begin{code} @@ -350,19 +347,6 @@ Stable A = ¬ ¬ A → A \end{code} Show that any negated formula is stable, and that the conjunction of two stable formulas is stable. -\begin{code} -postulate - - ¬-stable : ∀ {A : Set} - ------------ - → Stable (¬ A) - - ×-stable : ∀ {A B : Set} - → Stable A - → Stable B - -------------- - → Stable (A × B) -\end{code} ## Standard Prelude