From 81b5da1ebd33d017f6558a63d7d2d214f371056d Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 17 Mar 2018 11:51:09 -0300 Subject: [PATCH] moving LogicAns to NegationAns --- src/Logic.lagda | 48 +++++++++++++++---------------- src/LogicAns.lagda | 52 --------------------------------- src/Negation.lagda | 5 ++-- src/NegationAns.lagda | 67 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 94 insertions(+), 78 deletions(-) delete mode 100644 src/LogicAns.lagda create mode 100644 src/NegationAns.lagda diff --git a/src/Logic.lagda b/src/Logic.lagda index 15650026..f69db196 100644 --- a/src/Logic.lagda +++ b/src/Logic.lagda @@ -142,10 +142,10 @@ and similarly for `invʳ`, which does the same (up to renaming). ×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A) ×-comm = record - { to = λ { (x , y) → (y , x)} - ; fro = λ { (y , x) → (x , y)} - ; invˡ = λ { (x , y) → refl } - ; invʳ = λ { (y , x) → refl } + { to = λ { (x , y) → (y , x)} + ; from = λ { (y , x) → (x , y)} + ; from∘to = λ { (x , y) → refl } + ; to∘from = λ { (y , x) → refl } } \end{code} @@ -171,10 +171,10 @@ matching against a suitable pattern to enable simplificition. ×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C)) ×-assoc = record - { to = λ { ((x , y) , z) → (x , (y , z)) } - ; fro = λ { (x , (y , z)) → ((x , y) , z) } - ; invˡ = λ { ((x , y) , z) → refl } - ; invʳ = λ { (x , (y , z)) → refl } + { to = λ { ((x , y) , z) → (x , (y , z)) } + ; from = λ { (x , (y , z)) → ((x , y) , z) } + ; from∘to = λ { ((x , y) , z) → refl } + ; to∘from = λ { (x , (y , z)) → refl } } \end{code} @@ -237,10 +237,10 @@ a suitable pattern to enable simplification. ⊤-identityˡ : ∀ {A : Set} → (⊤ × A) ≃ A ⊤-identityˡ = record - { to = λ { (tt , x) → x } - ; fro = λ { x → (tt , x) } - ; invˡ = λ { (tt , x) → refl } - ; invʳ = λ { x → refl} + { to = λ { (tt , x) → x } + ; from = λ { x → (tt , x) } + ; from∘to = λ { (tt , x) → refl } + ; to∘from = λ { x → refl} } \end{code} @@ -343,18 +343,18 @@ does the same (up to renaming). \begin{code} ⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A) ⊎-comm = record - { to = λ { (inj₁ x) → (inj₂ x) - ; (inj₂ y) → (inj₁ y) - } - ; fro = λ { (inj₁ y) → (inj₂ y) - ; (inj₂ x) → (inj₁ x) - } - ; invˡ = λ { (inj₁ x) → refl - ; (inj₂ y) → refl - } - ; invʳ = λ { (inj₁ y) → refl - ; (inj₂ x) → refl - } + { to = λ { (inj₁ x) → (inj₂ x) + ; (inj₂ y) → (inj₁ y) + } + ; from = λ { (inj₁ y) → (inj₂ y) + ; (inj₂ x) → (inj₁ x) + } + ; from∘to = λ { (inj₁ x) → refl + ; (inj₂ y) → refl + } + ; to∘from = λ { (inj₁ y) → refl + ; (inj₂ x) → refl + } } \end{code} Being *commutative* is different from being *commutative up to diff --git a/src/LogicAns.lagda b/src/LogicAns.lagda deleted file mode 100644 index 30decfc8..00000000 --- a/src/LogicAns.lagda +++ /dev/null @@ -1,52 +0,0 @@ ---- -title : "Logic Answers" -layout : page -permalink : /LogicAns ---- - -\begin{code} -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) -open import Isomorphism using (_≃_) -open import Logic -\end{code} - - -*Equivalences for classical logic* - -\begin{code} -ex1 : ¬¬-elim → excluded-middle -ex1 h = h excluded-middle-irrefutable - -ex2 : excluded-middle → implication -ex2 em f with em -... | inj₁ a = inj₂ (f a) -... | inj₂ ¬a = inj₁ ¬a - -ex3 : excluded-middle → peirce -ex3 em k with em -... | inj₁ a = a -... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a)) - -help′ : excluded-middle → ∀ {A B : Set} → ¬ (A × B) → ¬ A ⊎ ¬ B -help′ em ¬a×b with em | em -... | inj₁ a | inj₁ b = ⊥-elim (¬a×b (a , b)) -... | inj₁ a | inj₂ ¬b = inj₂ ¬b -... | inj₂ ¬a | inj₁ b = inj₁ ¬a -... | inj₂ ¬a | inj₂ ¬b = inj₁ ¬a - -⊤⊥-iso : (¬ ⊥) ≃ ⊤ -⊤⊥-iso = - record - { to = λ _ → tt - ; fro = λ _ ff → ff - ; invˡ = λ _ → extensionality (λ ()) - ; invʳ = λ { tt → refl } - } -\end{code} - -*Existentials and Universals* - -\begin{code} -∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x) -∃¬¬∀ (x , ¬bx) ∀bx = ¬bx (∀bx x) -\end{code} diff --git a/src/Negation.lagda b/src/Negation.lagda index 59c94da2..9d7e5d64 100644 --- a/src/Negation.lagda +++ b/src/Negation.lagda @@ -265,13 +265,14 @@ Philip Wadler, *International Conference on Functional Programming*, 2003.) ### Exercise -Prove the following three formulas are equivalent to each other, -and to the formulas `EM` and `⊎-Dual-+` given earlier. +Prove the following four formulas are equivalent to each other, +and to the formula `EM` given earlier. \begin{code} ¬¬-Elim Peirce Implication : Set₁ ¬¬-Elim = ∀ {A : Set} → ¬ ¬ A → A Peirce = ∀ {A B : Set} → (((A → B) → A) → A) Implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B +×-Implies-⊎ = ∀ {A B : Set} → ¬ (A × B) → (¬ A) ⊎ (¬ B) \end{code} diff --git a/src/NegationAns.lagda b/src/NegationAns.lagda new file mode 100644 index 00000000..a949d552 --- /dev/null +++ b/src/NegationAns.lagda @@ -0,0 +1,67 @@ +--- +title : "Logic Answers" +layout : page +permalink : /LogicAns +--- + +\begin{code} +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-⊎) +\end{code} + +In what follows, we occasionally require [extensionality][extensionality]. +\begin{code} +postulate + extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g +\end{code} + +[extensionality]: Equality/index.html#extensionality + + + +*Equivalences for classical logic* + +\begin{code} +ex1 : ¬¬-Elim → EM +ex1 h = h em-irrefutable + +ex2 : EM → Implication +ex2 em f with em +... | inj₁ a = inj₂ (f a) +... | inj₂ ¬a = inj₁ ¬a + +ex3 : EM → Peirce +ex3 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 + +⊤⊥-iso : (¬ ⊥) ≃ ⊤ +⊤⊥-iso = + record + { to = λ{ _ → tt } + ; from = λ{ _ → id } + ; from∘to = λ{ _ → extensionality (λ ()) } + ; to∘from = λ{ tt → refl } + } +\end{code} + +*Existentials and Universals* + +\begin{code} +{- +∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x) +∃¬¬∀ (x , ¬bx) ∀bx = ¬bx (∀bx x) +-} +\end{code}