negation exercises
This commit is contained in:
parent
6c5aa96ef1
commit
a61fdc87ff
3 changed files with 80 additions and 53 deletions
|
@ -9,10 +9,11 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
|
||||||
open import Data.Unit using (⊤; tt)
|
open import Data.Unit using (⊤; tt)
|
||||||
open import Data.Empty using (⊥; ⊥-elim)
|
open import Data.Empty using (⊥; ⊥-elim)
|
||||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||||
open import Data.Product using (_×_; _,_; proj₁; proj₂)
|
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
|
||||||
open import Isomorphism using (_≃_)
|
open import Relation.Nullary using (¬_)
|
||||||
open import Negation using
|
-- open import Isomorphism using (_≃_)
|
||||||
(¬_; id; EM; em-irrefutable; ¬¬-Elim; Peirce; Implication; ×-Implies-⊎)
|
-- open import Negation using
|
||||||
|
-- (¬_; id; EM; em-irrefutable; ¬¬-Elim; Peirce; Implication; ×-Implies-⊎)
|
||||||
\end{code}
|
\end{code}
|
||||||
|
|
||||||
In what follows, we occasionally require [extensionality][extensionality].
|
In what follows, we occasionally require [extensionality][extensionality].
|
||||||
|
@ -28,25 +29,66 @@ postulate
|
||||||
*Equivalences for classical logic*
|
*Equivalences for classical logic*
|
||||||
|
|
||||||
\begin{code}
|
\begin{code}
|
||||||
ex1 : ¬¬-Elim → EM
|
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
|
||||||
ex1 h = h em-irrefutable
|
em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })
|
||||||
|
|
||||||
ex2 : EM → Implication
|
EM : Set₁
|
||||||
ex2 em f with em
|
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₂ (f a)
|
||||||
... | inj₂ ¬a = inj₁ ¬a
|
... | inj₂ ¬a = inj₁ ¬a
|
||||||
|
|
||||||
ex3 : EM → Peirce
|
ex4 : Implication → EM
|
||||||
ex3 em k with 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 = a
|
||||||
... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a))
|
... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a))
|
||||||
|
|
||||||
ex4 : EM → ×-Implies-⊎
|
ex6 : Peirce → EM
|
||||||
ex4 em ¬a×b with em | em
|
ex6 peirce = peirce (λ ¬em → ⊥-elim (em-irrefutable ¬em))
|
||||||
... | inj₁ a | inj₁ b = ⊥-elim (¬a×b (a , b))
|
|
||||||
... | inj₁ a | inj₂ ¬b = inj₂ ¬b
|
|
||||||
... | inj₂ ¬a | _ = inj₁ ¬a
|
|
||||||
|
|
||||||
|
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 : (¬ ⊥) ≃ ⊤
|
||||||
⊤⊥-iso =
|
⊤⊥-iso =
|
||||||
record
|
record
|
||||||
|
@ -55,6 +97,7 @@ ex4 em ¬a×b with em | em
|
||||||
; from∘to = λ{ _ → extensionality (λ ()) }
|
; from∘to = λ{ _ → extensionality (λ ()) }
|
||||||
; to∘from = λ{ tt → refl }
|
; to∘from = λ{ tt → refl }
|
||||||
}
|
}
|
||||||
|
-}
|
||||||
\end{code}
|
\end{code}
|
||||||
|
|
||||||
*Existentials and Universals*
|
*Existentials and Universals*
|
||||||
|
|
|
@ -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.
|
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.
|
Show that a disjunct of conjuncts implies a conjunct of disjuncts.
|
||||||
\begin{code}
|
\begin{code}
|
||||||
|
@ -809,7 +809,7 @@ postulate
|
||||||
Does the converse hold? If so, prove; if not, give a counterexample.
|
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.
|
Define equivalence of propositions (also known as "if and only if") as follows.
|
||||||
\begin{code}
|
\begin{code}
|
||||||
|
|
|
@ -156,14 +156,14 @@ the other.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
### Exercise (`≢`, `<-irrerflexive`)
|
### Exercise `<-irrerflexive`
|
||||||
|
|
||||||
Using negation, show that
|
Using negation, show that
|
||||||
[strict inequality]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#strict-inequality)
|
[strict inequality]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#strict-inequality)
|
||||||
is irreflexive, that is, `n < n` holds for no `n`.
|
is irreflexive, that is, `n < n` holds for no `n`.
|
||||||
|
|
||||||
|
|
||||||
### Exercise (`trichotomy`)
|
### Exercise `trichotomy`
|
||||||
|
|
||||||
Show that strict inequality satisfies
|
Show that strict inequality satisfies
|
||||||
[trichotomy]({{ site.baseurl }}{% link out/plfa/Relations.md %}/#trichotomy),
|
[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.
|
negation of the other two.
|
||||||
|
|
||||||
|
|
||||||
### Exercise (`⊎-dual-×`)
|
### Exercise `⊎-dual-×`
|
||||||
|
|
||||||
Show that conjunction, disjunction, and negation are related by a
|
Show that conjunction, disjunction, and negation are related by a
|
||||||
version of De Morgan's Law.
|
version of De Morgan's Law.
|
||||||
\begin{code}
|
|
||||||
postulate
|
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
|
||||||
⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
|
|
||||||
\end{code}
|
|
||||||
This result is an easy consequence of something we've proved previously.
|
This result is an easy consequence of something we've proved previously.
|
||||||
|
|
||||||
Is there also a term of the following type?
|
Is there also a term of the following type?
|
||||||
\begin{code}
|
|
||||||
postulate
|
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
|
||||||
×-dual-⊎ : ∀ {A B : Set} → ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
|
|
||||||
\end{code}
|
|
||||||
If so, prove; if not, explain why.
|
If so, prove; if not, explain why.
|
||||||
|
|
||||||
|
|
||||||
|
@ -327,21 +325,20 @@ just handed to him.
|
||||||
Philip Wadler, _International Conference on Functional Programming_, 2003.)
|
Philip Wadler, _International Conference on Functional Programming_, 2003.)
|
||||||
|
|
||||||
|
|
||||||
#### Exercise
|
#### Exercise `classical` (stretch)
|
||||||
|
|
||||||
Consider the following five terms of the given types.
|
Consider the following principles.
|
||||||
\begin{code}
|
|
||||||
postulate
|
* Excluded Middle: `A ⊎ ¬ A`, for all `A`
|
||||||
em′ : ∀ {A : Set} → A ⊎ ¬ A
|
* Double Negation Elimination: `¬ ¬ A → A`, for all `A`
|
||||||
¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A
|
* Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
|
||||||
peirce : ∀ {A B : Set} → (((A → B) → A) → A)
|
* Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
|
||||||
→-implies-⊎ : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
|
* De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
|
||||||
×-implies-⊎ : ∀ {A B : Set} → ¬ (A × B) → (¬ A) ⊎ (¬ B)
|
|
||||||
\end{code}
|
Show that each of these implies all the others.
|
||||||
Show that given any one term of the specified type, we can derive the others.
|
|
||||||
|
|
||||||
|
|
||||||
### Exercise (`¬-stable`, `×-stable`)
|
#### Exercise `stable` (stretch)
|
||||||
|
|
||||||
Say that a formula is _stable_ if double negation elimination holds for it.
|
Say that a formula is _stable_ if double negation elimination holds for it.
|
||||||
\begin{code}
|
\begin{code}
|
||||||
|
@ -350,19 +347,6 @@ Stable A = ¬ ¬ A → A
|
||||||
\end{code}
|
\end{code}
|
||||||
Show that any negated formula is stable, and that the conjunction
|
Show that any negated formula is stable, and that the conjunction
|
||||||
of two stable formulas is stable.
|
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
|
## Standard Prelude
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue