From 7d516c8a9f166fd501c4e5a63b5f0c81e90cc040 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 5 Jan 2018 21:30:39 -0200 Subject: [PATCH] added Logic --- index.md | 3 + src/Logic.lagda | 170 +++++++++++++++++++++++++++++++++++ src/Naturals.lagda | 5 +- src/Properties.lagda | 2 +- src/Relations.lagda | 2 +- src/{ => extra}/EvenOdd.agda | 14 ++- 6 files changed, 188 insertions(+), 8 deletions(-) create mode 100644 src/Logic.lagda rename src/{ => extra}/EvenOdd.agda (83%) diff --git a/index.md b/index.md index 45aca764..0176745a 100644 --- a/index.md +++ b/index.md @@ -23,6 +23,9 @@ http://homepages.inf.ed.ac.uk/wadler/ - [Naturals: Natural numbers]({{ "/Naturals" | relative_url }}) - [Properties: Proof by induction]({{ "/Properties" | relative_url }}) + - [PropertiesEx: Solutions to exercises]({{ "/PropertiesEx" | relative_url }}) + - [Relations: Inductive Definition of Relations]({{ "/Relations" | relative_url }}) + - [RelationsEx: Solutions to exercises]({{ "/RelationsEx" | relative_url }}) - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }}) - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }}) - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }}) diff --git a/src/Logic.lagda b/src/Logic.lagda new file mode 100644 index 00000000..38b38661 --- /dev/null +++ b/src/Logic.lagda @@ -0,0 +1,170 @@ +--- +title : "Logic: Propositions as Type" +layout : page +permalink : /Logic +--- + +This chapter describes the connection between logical connectives +(conjunction, disjunction, implication, for all, there exists, +equivalence) and datatypes (product, sum, function, dependent +function, dependent product, Martin Löf equivalence). + +## Imports + +\begin{code} +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +\end{code} + +## Conjunction + +Given two propositions `A` and `B`, the conjunction `A × B` holds +if both `A` holds and `B` holds. We formalise this idea by +declaring a suitable inductive type. +\begin{code} +data _×_ : Set → Set → Set where + _,_ : ∀ {A B : Set} → A → B → A × B +\end{code} +If `A` and `B` are propositions then `A × B` is +also a proposition. Evidence that `A × B` holds is of the form +`a , b`, where `a` is evidence that `A` holds and +`b` is evidence that `B` holds. + +We set the precedence of conjunction so that it binds less +tightly than anything save disjunction, and of the pairing +operator so that it binds less tightly than any arithmetic +operator. +\begin{code} +infixr 2 _×_ +infixr 4 _,_ +\end{code} + + + +## Disjunction + +Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds +if either `A` holds or `B` holds. We formalise this idea by +declaring a suitable inductive type. +\begin{code} +data _⊎_ : Set → Set → Set where + inj₁ : ∀ {A B : Set} → A → A ⊎ B + inj₂ : ∀ {A B : Set} → B → A ⊎ B +\end{code} +If `A` and `B` are propositions then `A ⊎ B` is +also a proposition. Evidence that `A ⊎ B` holds is either of the form +`inj₁ a`, where `a` is evidence that `A` holds, or `inj₂ b`, where +`b` is evidence that `B` holds. + +We set the precedence of disjunction so that it binds less tightly +than any other operator. +\begin{code} +infix 1 _⊎_ +\end{code} +Thus, `m ≤ n ⊎ n ≤ m` parses as `(m ≤ n) ⊎ (n ≤ m)`, +and `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`. + +## Distribution + +Distribution of `×` over `⊎` is an isomorphism. +\begin{code} +data _≃_ : Set → Set → Set where + iso : ∀ {A B : Set} → (f : A → B) → (g : B → A) → + (∀ (x : A) → g (f x) ≡ x) → (∀ (y : B) → f (g y) ≡ y) → A ≃ B + +×-distributes-+ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C)) +×-distributes-+ = iso f g gf fg + where + + f : ∀ {A B C : Set} → (A ⊎ B) × C → (A × C) ⊎ (B × C) + f (inj₁ a , c) = inj₁ (a , c) + f (inj₂ b , c) = inj₂ (b , c) + + g : ∀ {A B C : Set} → (A × C) ⊎ (B × C) → (A ⊎ B) × C + g (inj₁ (a , c)) = (inj₁ a , c) + g (inj₂ (b , c)) = (inj₂ b , c) + + gf : ∀ {A B C : Set} → (x : (A ⊎ B) × C) → g (f x) ≡ x + gf (inj₁ a , c) = refl + gf (inj₂ b , c) = refl + + fg : ∀ {A B C : Set} → (y : (A × C) ⊎ (B × C)) → f (g y) ≡ y + fg (inj₁ (a , c)) = refl + fg (inj₂ (b , c)) = refl +\end{code} + +Distribution of `⊎` over `×` is half an isomorphism. +\begin{code} +data _≃ʳ_ : Set → Set → Set where + isoʳ : ∀ {A B : Set} → (f : A → B) → (g : B → A) → + (∀ (x : A) → g (f x) ≡ x) → A ≃ʳ B + ++-distributes-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≃ʳ ((A ⊎ C) × (B ⊎ C)) ++-distributes-× = isoʳ f g gf + where + + f : ∀ {A B C : Set} → (A × B) ⊎ C → (A ⊎ C) × (B ⊎ C) + f (inj₁ (a , b)) = (inj₁ a , inj₁ b) + f (inj₂ c) = (inj₂ c , inj₂ c) + + g : ∀ {A B C : Set} → (A ⊎ C) × (B ⊎ C) → (A × B) ⊎ C + g (inj₁ a , inj₁ b) = inj₁ (a , b) + g (inj₁ a , inj₂ c) = inj₂ c + g (inj₂ c , inj₁ b) = inj₂ c + g (inj₂ c , inj₂ c′) = inj₂ c -- or inj₂ c′ + + gf : ∀ {A B C : Set} → (x : (A × B) ⊎ C) → g (f x) ≡ x + gf (inj₁ (a , b)) = refl + gf (inj₂ c) = refl +\end{code} + +## True + +\begin{code} +data ⊤ : Set where + tt : ⊤ +\end{code} + +## False + +\begin{code} +data ⊥ : Set where + -- no clauses! + +⊥-elim : {A : Set} → ⊥ → A +⊥-elim () +\end{code} + +## Implication + +## Negation + +\begin{code} +¬_ : Set → Set +¬ A = A → ⊥ + +infix 3 ¬_ + +data Dec : Set → Set where + yes : ∀ {A : Set} → A → Dec A + no : ∀ {A : Set} → (¬ A) → Dec A + +contraposition : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A) +contraposition f ¬b a = ¬b (f a) +\end{code} + + + +## Intuitive and Classical logic + +## Universals + +## Existentials + +## Equivalence + +## Unicode + +This chapter introduces the following unicode. + + ≤ U+2264 LESS-THAN OR EQUAL TO (\<=, \le) + diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 52b19305..10cb8a54 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -563,8 +563,9 @@ of the logarithms of *m* and *n*. ## Unicode -In each chapter, we will list at the end all unicode characters. -In this chapter we use the following. +In each chapter, we will list at the end all unicode characters that +first appear in that chapter. This chapter introduces the following +unicode. ℕ U+2115 DOUBLE-STRUCK CAPITAL N (\bN) → U+2192 RIGHTWARDS ARROW (\to, \r) diff --git a/src/Properties.lagda b/src/Properties.lagda index 012317ab..3bf164a6 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -616,7 +616,7 @@ right. ## Unicode -In this chapter we introduced the following unicode. +This chapter introduces the following unicode. ≡ U+2261 IDENTICAL TO (\==) ∀ U+2200 FOR ALL (\forall) diff --git a/src/Relations.lagda b/src/Relations.lagda index 78ce3d5d..1d06910d 100644 --- a/src/Relations.lagda +++ b/src/Relations.lagda @@ -481,7 +481,7 @@ the keyword `where`. --> ## Unicode -In this chapter we use the following unicode. +This chapter introduces the following unicode. ≤ U+2264 LESS-THAN OR EQUAL TO (\<=, \le) ˡ U+02E1 MODIFIER LETTER SMALL L (\^l) diff --git a/src/EvenOdd.agda b/src/extra/EvenOdd.agda similarity index 83% rename from src/EvenOdd.agda rename to src/extra/EvenOdd.agda index f8ab288a..9fdf2e0f 100644 --- a/src/EvenOdd.agda +++ b/src/extra/EvenOdd.agda @@ -21,12 +21,9 @@ mutual data odd : ℕ → Set where suc : ∀ {n : ℕ} → even n → odd (suc n) -+-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0) ++-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0) +-lemma m rewrite +-identity m | +-suc m m = refl -+-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0) -+-lemma′ m rewrite +-suc m (m + 0) = {!!} - mutual is-even : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m) is-even zero zero = zero , refl @@ -36,3 +33,12 @@ mutual is-odd : ∀ (n : ℕ) → odd n → ∃(λ (m : ℕ) → n ≡ 1 + 2 * m) is-odd (suc n) (suc evenn) with is-even n evenn ... | m , n≡2*m rewrite n≡2*m = m , refl + ++-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0) ++-lemma′ m rewrite +-suc m (m + 0) = {!!} + +is-even′ : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m) +is-even′ zero zero = zero , refl +is-even′ (suc n) (suc oddn) with is-odd n oddn +... | m , n≡1+2*m rewrite n≡1+2*m | +-identity m | +-suc m m = suc m , {!!} +