From 6ae06a223641a3005283f38045e0ef9449f75643 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 26 Jan 2018 19:35:55 -0200 Subject: [PATCH] further progress on Logic --- out/Logic.md | 2648 +++++++++++++++++++++++++++++------------------ src/Logic.lagda | 21 +- 2 files changed, 1648 insertions(+), 1021 deletions(-) diff --git a/out/Logic.md b/out/Logic.md index 9684bd31..cb0e47ab 100644 --- a/out/Logic.md +++ b/out/Logic.md @@ -12380,210 +12380,833 @@ instantiate that proof that `∀ (x : A) → B[x] → C` to any `x`, and we may choose the particular `x` provided by the evidence that `∃ (λ (x : A) → B[x])`. +The types `¬ (∃ (λ (x : A) → B[x]))` and `∀ (x : A) → ¬ B[x]` are isomorphic. +
{% raw %}
+extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
+extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
+
+¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃ (λ (x : A) → B x)) ≃ ∀ (x : A) → ¬ B x
+¬∃∀ =
+  record
+    { to   =  λ { ¬∃bx x bx → ¬∃bx (x , bx) }
+    ; fro  =  λ { ∀¬bx (x , bx) → ∀¬bx x bx }
+    ; invˡ =  λ { ¬∃bx → extensionality (λ { (x , bx) → refl }) } 
+    ; invʳ =  λ { ∀¬bx → refl } 
+    }
+{% endraw %}
+ + + [It would be better to have even and odd as an exercise. Is there a simpler example that I could start with?] As an example, recall the definitions of `even` and `odd` from Chapter [Relations](Relations). 
{% raw %}
-mutual
   data even : ℕ → Set where
     ev-zero : even zero
     ev-suc : ∀ {n : ℕ} → odd n → even (suc n)
   data odd : ℕ → Set where
     od-suc : ∀ {n : ℕ} → even n → odd (suc n)
 {% endraw %}
@@ -12591,494 +13214,142 @@ We show that a number `n` is even if and only if there exists another number `m` such that `n ≡ 2 * m`, and is odd if and only if there is another number `m` such that `n ≡ 1 + 2 * m`. -Here is the proof in the forward direction. -
{% raw %}
-
+
 ## Decidability
 
-\begin{code}
-{% raw %}
+data Dec : Set → Set where
-  yes : ∀ {A : Set} → A → Dec A
-  no  : ∀ {A : Set} → (¬ A) → Dec A
-{% endraw %}
- -## Decidability - -
{% raw %}
-dem1 : ∀ {A B : Set} → A × B → ¬ (¬ A ⊎ ¬ B)
-dem1 (a , b) (inj₁ ¬a) = ¬a a
-dem1 (a , b) (inj₂ ¬b) = ¬b b
-
-dem2 : ∀ {A B : Set} → A ⊎ BDec →: ¬Set (¬→ ASet × ¬ B)where
-dem2yes (inj₁: ∀ a){A (¬a: ,Set} ¬b)→ =A ¬a→ aDec A
-dem2 (inj₂no  : b)∀ (¬a{A : ,Set} ¬b→ (¬ A) =→ ¬bDec bA
 {% endraw %}
@@ -13098,592 +13369,620 @@ Two halves of de Morgan's laws hold intuitionistically. The other two halves are each equivalent to the law of double negation. 
{% raw %}
-dem-≃dem1 : ∀ {A B : Set} → (¬ (A ⊎ B)) ≃ (¬ A × ¬ B → ¬ (¬ A ⊎ ¬ B)
 dem-≃dem1 (a , b) (inj₁ ¬a) = →-distributes-⊎¬a a
+dem1 (a , b) (inj₂ ¬b) = ¬b b
+
+dem2 : ∀ {A B : Set} → A ⊎ B → ¬ (¬ A × ¬ B)
+dem2 (inj₁ a) (¬a , ¬b) = ¬a a
+dem2 (inj₂ b) (¬a , ¬b) = ¬b b
 {% endraw %}
For the other variant of De Morgan's law, one way is an isomorphism. 
{% raw %}
-dem-halfdem-≃ : ∀ {A B : Set} → (¬ (A ⊎ ¬ B)) →≃ ¬ (¬ A × ¬ B)
 dem-halfdem-≃ (inj₁ ¬a) (a , b) = ¬a a
-dem-half (inj₂ ¬b) (a , b) = ¬b b→-distributes-⊎
 {% endraw %}
The other holds in only one direction. 
{% raw %}
-implication-inv : ∀ {A B : Set} → (¬ A ⊎ B) → A → B
-implication-inv (inj₁ ¬a) adem-half =: ⊥-elim∀ {A B (¬a: aSet)}
-implication-inv → ¬ A ⊎ ¬ B → ¬ (inj₂A b× B)  a = b
-
 demorgan-invdem-half (inj₁ ¬a) (a :, ∀b) {A= B¬a :a
+dem-half Set} → A ⊎ B → ¬ (¬inj₂ ¬b) A × ¬ B)
-demorgan-inv (inj₁ a) (¬a , ¬b) =  ¬a a
-demorgan-inv (inj₂ b) (¬a , ¬b) =  ¬b ¬b b
 {% endraw %}
@@ -13694,6 +13993,321 @@ intuitionistically or equivalent to classical logic. For several of the laws equivalent to classical logic, the reverse direction holds in intuitionistic long. +
{% raw %}
+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
+{% endraw %}
diff --git a/src/Logic.lagda b/src/Logic.lagda index 9554423a..c4400942 100644 --- a/src/Logic.lagda +++ b/src/Logic.lagda @@ -1171,6 +1171,23 @@ instantiate that proof that `∀ (x : A) → B[x] → C` to any `x`, and we may choose the particular `x` provided by the evidence that `∃ (λ (x : A) → B[x])`. +The types `¬ (∃ (λ (x : A) → B[x]))` and `∀ (x : A) → ¬ B[x]` are isomorphic. +\begin{code} +extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g +extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y)) + +¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃ (λ (x : A) → B x)) ≃ ∀ (x : A) → ¬ B x +¬∃∀ = + record + { to = λ { ¬∃bx x bx → ¬∃bx (x , bx) } + ; fro = λ { ∀¬bx (x , bx) → ∀¬bx x bx } + ; invˡ = λ { ¬∃bx → extensionality (λ { (x , bx) → refl }) } + ; invʳ = λ { ∀¬bx → refl } + } +\end{code} + + + [It would be better to have even and odd as an exercise. Is there a simpler example that I could start with?] @@ -1188,10 +1205,6 @@ We show that a number `n` is even if and only if there exists another number `m` such that `n ≡ 2 * m`, and is odd if and only if there is another number `m` such that `n ≡ 1 + 2 * m`. -Here is the proof in the forward direction. -\begin{code} - -\end{code} ## Decidability