diff --git a/src/Connectives-old.lagda b/src/Connectives-old.lagda deleted file mode 100644 index fc8ba6b9..00000000 --- a/src/Connectives-old.lagda +++ /dev/null @@ -1,817 +0,0 @@ ---- -title : "Connectives: Conjunction, Disjunction, and Implication" -layout : page -permalink : /Connectives ---- - -This chapter introduces the basic logical connectives, by observing -a correspondence between connectives of logic and data types, -a principal known as *Propositions as Types*. - -+ *conjunction* is *product* -+ *disjunction* is *sum* -+ *true* is *unit type* -+ *false* is *empty type* -+ *implication* is *function space* - - -## Imports - -\begin{code} -import Relation.Binary.PropositionalEquality as Eq -open Eq using (_≡_; refl; sym; trans; cong) -open Eq.≡-Reasoning -open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_) -open Isomorphism.≃-Reasoning -open import Data.Nat using (ℕ; zero; suc; _+_; _*_) -open import Data.Nat.Properties.Simple using (+-suc) -open import Function using (_∘_) -\end{code} - -We assume [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 - - -## Conjunction is product - -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} -Evidence that `A × B` holds is of the form -`(M , N)`, where `M` is evidence that `A` holds and -`N` is evidence that `B` holds. By convention, we -parenthesise pairs, even though `M , N` is also -accepted by Agda. - -Given evidence that `A × B` holds, we can conclude that either -`A` holds or `B` holds. -\begin{code} -proj₁ : ∀ {A B : Set} → A × B → A -proj₁ (x , y) = x - -proj₂ : ∀ {A B : Set} → A × B → B -proj₂ (x , y) = y -\end{code} -If `L` is evidence that `A × B` holds, then `fst L` is evidence -that `A` holds, and `proj₂ L` is evidence that `B` holds. - -Equivalently, we could also declare conjunction as a record type. -\begin{code} -record _×′_ (A B : Set) : Set where - field - proj₁′ : A - proj₂′ : B -open _×′_ -\end{code} -Here record construction - - record - { proj₁′ = M - ; proj₂′ = N - } - -corresponds to the term - - ( M , N ) - -where `M` is a term of type `A` and `N` is a term of type `B`. - -When `(_,_)` appears on the right-hand side of an equation we -refer to it as a *constructor*, and when it appears on the -left-hand side we refer to it as a *destructor*. We also refer -to `proj₁` and `proj₂` as destructors, since they play a similar role. -Other terminology refers to constructor as *introducing* a conjunction, -and to a destructor as *eliminating* a conjunction. -Indeed, `proj₁` and `proj₂` are sometimes given the names -`×-elim₁` and `×-elim₂`. - -Applying each destructor and reassembling the results with the -constructor is the identity over products. -\begin{code} -η-× : ∀ {A B : Set} (w : A × B) → (proj₁ w , proj₂ w) ≡ w -η-× (x , y) = refl -\end{code} -The pattern matching on the left-hand side is essential, since -replacing `w` by `(x , y)` allows both sides of the equation to -simplify to the same term. - -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} -Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and -`(m * n , p)` parses as `((m * n) , p)`. - -Given two types `A` and `B`, we refer to `A x B` as the -*product* of `A` and `B`. In set theory, it is also sometimes -called the *cartesian product*, and in computing it corresponds -to a *record* type. Among other reasons for -calling it the product, note that if type `A` has `m` -distinct members, and type `B` has `n` distinct members, -then the type `A × B` has `m * n` distinct members. -For instance, consider a type `Bool` with two members, and -a type `Tri` with three members. -\begin{code} -data Bool : Set where - true : Bool - false : Bool - -data Tri : Set where - aa : Tri - bb : Tri - cc : Tri -\end{code} -Then the type `Bool × Tri` has six members: - - (true , aa) (true , bb) (true , cc) - (false , aa) (false , bb) (false , cc) - -For example, the following function enumerates all -possible arguments of type `Bool × Tri`: -\begin{code} -×-count : Bool × Tri → ℕ -×-count (true , aa) = 1 -×-count (true , bb) = 2 -×-count (true , cc) = 3 -×-count (false , aa) = 4 -×-count (false , bb) = 5 -×-count (false , cc) = 6 -\end{code} - -Product on types also shares a property with product on numbers in -that there is a sense in which it is commutative and associative. In -particular, product is commutative and associative *up to -isomorphism*. - -For commutativity, the `to` function swaps a pair, taking `(x , y)` to -`(y , x)`, and the `from` function does the same (up to renaming). -Instantiating the patterns correctly in `from∘to` and `to∘from` is essential. -Replacing the definition of `from∘to` by `λ w → refl` will not work; -and similarly for `to∘from`, which does the same (up to renaming). -\begin{code} -×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A) -×-comm = - record - { to = λ{ (x , y) → (y , x)} - ; from = λ{ (y , x) → (x , y)} - ; from∘to = λ{ (x , y) → refl } - ; to∘from = λ{ (y , x) → refl } - } -\end{code} - -Being *commutative* is different from being *commutative up to -isomorphism*. Compare the two statements: - - m * n ≡ n * m - A × B ≃ B × A - -In the first case, we might have that `m` is `2` and `n` is `3`, and -both `m * n` and `n * m` are equal to `6`. In the second case, we -might have that `A` is `Bool` and `B` is `Tri`, and `Bool × Tri` is -*not* the same as `Tri × Bool`. But there is an isomorphism -between the two types. For -instance, `(true , aa)`, which is a member of the former, corresponds -to `(aa , true)`, which is a member of the latter. - -For associativity, the `to` function reassociates two uses of pairing, -taking `((x , y) , z)` to `(x , (y , z))`, and the `from` function does -the inverse. Again, the evidence of left and right inverse requires -matching against a suitable pattern to enable simplification. -\begin{code} -×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C)) -×-assoc = - record - { 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} - -Being *associative* is not the same as being *associative -up to isomorphism*. Compare the two statements: - - (m * n) * p ≡ m * (n * p) - (A × B) × C ≃ A × (B × C) - -For example, the type `(ℕ × Bool) × Tri` is *not* the same as `ℕ × -(Bool × Tri)`. But there is an isomorphism between the two types. For -instance `((1 , true) , aa)`, which is a member of the former, -corresponds to `(1 , (true , aa))`, which is a member of the latter. - -## Truth is unit - -Truth `⊤` always holds. We formalise this idea by -declaring a suitable inductive type. -\begin{code} -data ⊤ : Set where - tt : ⊤ -\end{code} -Evidence that `⊤` holds is of the form `tt`. - -Given evidence that `⊤` holds, there is nothing more of interest we -can conclude. Since truth always holds, knowing that it holds tells -us nothing new. - -The nullary case of `η-×` is `η-⊤`, which asserts that any -term of type `⊤` must be equal to `tt`. -\begin{code} -η-⊤ : ∀ (w : ⊤) → tt ≡ w -η-⊤ tt = refl -\end{code} -The pattern matching on the left-hand side is essential. Replacing -`w` by `tt` allows both sides of the equation to simplify to the -same term. - -We refer to `⊤` as the *unit* type. And, indeed, -type `⊤` has exactly once member, `tt`. For example, the following -function enumerates all possible arguments of type `⊤`: -\begin{code} -⊤-count : ⊤ → ℕ -⊤-count tt = 1 -\end{code} - -For numbers, one is the identity of multiplication. Correspondingly, -unit is the identity of product *up to isomorphism*. For left -identity, the `to` function takes `(tt , x)` to `x`, and the `from` -function does the inverse. The evidence of left inverse requires -matching against a suitable pattern to enable simplification. -\begin{code} -⊤-identityˡ : ∀ {A : Set} → (⊤ × A) ≃ A -⊤-identityˡ = - record - { to = λ{ (tt , x) → x } - ; from = λ{ x → (tt , x) } - ; from∘to = λ{ (tt , x) → refl } - ; to∘from = λ{ x → refl } - } -\end{code} - -Having an *identity* is different from having an identity -*up to isomorphism*. Compare the two statements: - - 1 * m ≡ m - ⊤ × A ≃ A - -In the first case, we might have that `m` is `2`, and both -`1 * m` and `m` are equal to `2`. In the second -case, we might have that `A` is `Bool`, and `⊤ × Bool` is *not* the -same as `Bool`. But there is an isomorphism between the two types. -For instance, `(tt, true)`, which is a member of the former, -corresponds to `true`, which is a member of the latter. - -Right identity follows from commutativity of product and left identity. -\begin{code} -⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A -⊤-identityʳ {A} = - ≃-begin - (A × ⊤) - ≃⟨ ×-comm ⟩ - (⊤ × A) - ≃⟨ ⊤-identityˡ ⟩ - A - ≃-∎ -\end{code} -Here we have used a chain of isomorphisms, -analogous to that used for equality. - - -## Disjunction is sum - -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} -Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M` -is evidence that `A` holds, or `inj₂ N`, where `N` is evidence that -`B` holds. - -Given evidence that `A → C` and `B → C` both hold, then given -evidence that `A ⊎ B` holds we can conclude that `C` holds. -\begin{code} -⊎-elim : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B → C) -⊎-elim f g (inj₁ x) = f x -⊎-elim f g (inj₂ y) = g y -\end{code} -Pattern matching against `inj₁` and `inj₂` is typical of how we exploit -evidence that a disjunction holds. - -When `inj₁` and `inj₂` appear on the right-hand side of an equation we -refer to them as *constructors*, and when they appears on the -left-hand side we refer to them as *destructors*. We also refer -to `⊎-elim` as a destructor, since it plays a similar role. -Other terminology refers to constructors as *introducing* a disjunction, -and to a destructors as *eliminating* a disjunction. - -Applying the destructor to each of the constructors is the identity. -\begin{code} -η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → ⊎-elim inj₁ inj₂ w ≡ w -η-⊎ (inj₁ x) = refl -η-⊎ (inj₂ y) = refl -\end{code} -More generally, we can also throw in an arbitrary function from a disjunction. -\begin{code} -uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) → - ⊎-elim (h ∘ inj₁) (h ∘ inj₂) w ≡ h w -uniq-⊎ h (inj₁ x) = refl -uniq-⊎ h (inj₂ y) = refl -\end{code} -The pattern matching on the left-hand side is essential. Replacing -`w` by `inj₁ x` allows both sides of the equation to simplify to the -same term, and similarly for `inj₂ y`. - -We set the precedence of disjunction so that it binds less tightly -than any other declared operator. -\begin{code} -infix 1 _⊎_ -\end{code} -Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`. - -Given two types `A` and `B`, we refer to `A ⊎ B` as the -*sum* of `A` and `B`. In set theory, it is also sometimes -called the *disjoint union*, and in computing it corresponds -to a *variant record* type. Among other reasons for -calling it the sum, note that if type `A` has `m` -distinct members, and type `B` has `n` distinct members, -then the type `A ⊎ B` has `m + n` distinct members. -For instance, consider a type `Bool` with two members, and -a type `Tri` with three members, as defined earlier. -Then the type `Bool ⊎ Tri` has five -members: - - (inj₁ true) (inj₂ aa) - (inj₁ false) (inj₂ bb) - (inj₂ cc) - -For example, the following function enumerates all -possible arguments of type `Bool ⊎ Tri`: -\begin{code} -⊎-count : Bool ⊎ Tri → ℕ -⊎-count (inj₁ true) = 1 -⊎-count (inj₁ false) = 2 -⊎-count (inj₂ aa) = 3 -⊎-count (inj₂ bb) = 4 -⊎-count (inj₂ cc) = 5 -\end{code} - -Sum on types also shares a property with sum on numbers in that it is -commutative and associative *up to isomorphism*. - -For commutativity, the `to` function swaps the two constructors, -taking `inj₁ x` to `inj₂ x`, and `inj₂ y` to `inj₁ y`; and the `from` -function does the same (up to renaming). Replacing the definition of -`from∘to` by `λ w → refl` will not work; and similarly for `to∘from`, which -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) - } - ; 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 -isomorphism*. Compare the two statements: - - m + n ≡ n + m - A ⊎ B ≃ B ⊎ A - -In the first case, we might have that `m` is `2` and `n` is `3`, and -both `m + n` and `n + m` are equal to `5`. In the second case, we -might have that `A` is `Bool` and `B` is `Tri`, and `Bool ⊎ Tri` is -*not* the same as `Tri ⊎ Bool`. But there is an isomorphism between -the two types. For instance, `inj₁ true`, which is a member of the -former, corresponds to `inj₂ true`, which is a member of the latter. - -For associativity, the `to` function reassociates, and the `from` function does -the inverse. Again, the evidence of left and right inverse requires -matching against a suitable pattern to enable simplification. -\begin{code} -⊎-assoc : ∀ {A B C : Set} → ((A ⊎ B) ⊎ C) ≃ (A ⊎ (B ⊎ C)) -⊎-assoc = record - { to = λ{ (inj₁ (inj₁ x)) → (inj₁ x) - ; (inj₁ (inj₂ y)) → (inj₂ (inj₁ y)) - ; (inj₂ z) → (inj₂ (inj₂ z)) - } - ; from = λ{ (inj₁ x) → (inj₁ (inj₁ x)) - ; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y)) - ; (inj₂ (inj₂ z)) → (inj₂ z) - } - ; from∘to = λ{ (inj₁ (inj₁ x)) → refl - ; (inj₁ (inj₂ y)) → refl - ; (inj₂ z) → refl - } - ; to∘from = λ{ (inj₁ x) → refl - ; (inj₂ (inj₁ y)) → refl - ; (inj₂ (inj₂ z)) → refl - } - } -\end{code} - -Again, being *associative* is not the same as being *associative -up to isomorphism*. For example, the type `(ℕ + Bool) + Tri` -is *not* the same as `ℕ + (Bool + Tri)`. But there is an -isomorphism between the two types. For instance `inj₂ (inj₁ true)`, -which is a member of the former, corresponds to `inj₁ (inj₂ true)`, -which is a member of the latter. - -## False is empty - -False `⊥` never holds. We formalise this idea by declaring -a suitable inductive type. -\begin{code} -data ⊥ : Set where - -- no clauses! -\end{code} -There is no possible evidence that `⊥` holds. - -Given evidence that `⊥` holds, we might conclude anything! Since -false never holds, knowing that it holds tells us we are in a -paradoxical situation. This is a basic principle of logic, -known in medieval times by the latin phrase *ex falso*, -and known to children through phrases such as -"if pigs had wings, then I'd be the Queen of Sheba". -We formalise it as follows. -\begin{code} -⊥-elim : ∀ {A : Set} → ⊥ → A -⊥-elim () -\end{code} -This is our first use of the *absurd pattern* `()`. -Here since `⊥` is a type with no members, we indicate that it is -*never* possible to match against a value of this type by using -the pattern `()`. - -The nullary case of `uniq-⊎` is `uniq-⊥`, which asserts that `⊥-elim` -is equal to any arbitrary function from `⊥`. -\begin{code} -uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w -uniq-⊥ h () -\end{code} -The pattern matching on the left-hand side is essential. Using -the absurd pattern asserts there are no possible values for `w`, -so the equation holds trivially. - -We refer to `⊥` as *empty* type. And, indeed, -type `⊥` has no members. For example, the following function -enumerates all possible arguments of type `⊥`: -\begin{code} -⊥-count : ⊥ → ℕ -⊥-count () -\end{code} -Here again the absurd pattern `()` indicates that no value can match -type `⊥`. - -For numbers, zero is the identity of addition. Correspondingly, -empty is the identity of sums *up to isomorphism*. -For left identity, the `to` function observes that `inj₁ ()` can never arise, -and takes `inj₂ x` to `x`, and the `from` function -does the inverse. The evidence of left inverse requires matching against -a suitable pattern to enable simplification. -\begin{code} -⊥-identityˡ : ∀ {A : Set} → (⊥ ⊎ A) ≃ A -⊥-identityˡ = - record - { to = λ{ (inj₁ ()) - ; (inj₂ x) → x - } - ; from = λ{ x → inj₂ x - } - ; from∘to = λ{ (inj₁ ()) - ; (inj₂ x) → refl - } - ; to∘from = λ{ x → refl - } - } -\end{code} - -Having an *identity* is different from having an identity -*up to isomorphism*. Compare the two statements: - - 0 + m ≡ m - ⊥ ⊎ A ≃ A - -In the first case, we might have that `m` is `2`, and both `0 + m` and -`m` are equal to `2`. In the second case, we might have that `A` is -`Bool`, and `⊥ ⊎ Bool` is *not* the same as `Bool`. But there is an -isomorphism between the two types. For instance, `inj₂ true`, which is -a member of the former, corresponds to `true`, which is a member of -the latter. - -Right identity follows from commutativity of sum and left identity. -\begin{code} -⊥-identityʳ : ∀ {A : Set} → (A ⊎ ⊥) ≃ A -⊥-identityʳ {A} = - ≃-begin - (A ⊎ ⊥) - ≃⟨ ⊎-comm ⟩ - (⊥ ⊎ A) - ≃⟨ ⊥-identityˡ ⟩ - A - ≃-∎ -\end{code} - -## Implication is function {#implication} - -Given two propositions `A` and `B`, the implication `A → B` holds if -whenever `A` holds then `B` must also hold. We formalise implication using -the function type, which has appeared throughout this book. - -Evidence that `A → B` holds is of the form - - λ (x : A) → N x - -where `N x` is a term of type `B` containing as a free variable `x` of type `A`. -Given a term `L` providing evidence that `A → B` holds, and a term `M` -providing evidence that `A` holds, the term `L M` provides evidence that -`B` holds. In other words, evidence that `A → B` holds is a function that -converts evidence that `A` holds into evidence that `B` holds. - -Put another way, if we know that `A → B` and `A` both hold, -then we may conclude that `B` holds. -\begin{code} -→-elim : ∀ {A B : Set} → (A → B) → A → B -→-elim L M = L M -\end{code} -In medieval times, this rule was known by the name *modus ponens*. -It corresponds to function application. - -Defining a function, with an named definition or a lambda expression, -is referred to as *introducing* a function, -while applying a function is referred to as *eliminating* the function. - -Elimination followed by introduction is the identity. -\begin{code} -η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f -η-→ {A} {B} f = extensionality η-helper - where - η-helper : (x : A) → (λ (x : A) → f x) x ≡ f x - η-helper x = refl -\end{code} -The proof depends on extensionality. - - - -Implication binds less tightly than any other operator. Thus, `A ⊎ B → -B ⊎ A` parses as `(A ⊎ B) → (B ⊎ A)`. - -Given two types `A` and `B`, we refer to `A → B` as the *function* -space from `A` to `B`. It is also sometimes called the *exponential*, -with `B` raised to the `A` power. Among other reasons for calling -it the exponential, note that if type `A` has `m` distinct -members, and type `B` has `n` distinct members, then the type -`A → B` has `n ^ m` distinct members. For instance, consider a -type `Bool` with two members and a type `Tri` with three members, -as defined earlier. The the type `Bool → Tri` has nine (that is, -three squared) members: - - λ{true → aa; false → aa} λ{true → aa; false → bb} λ{true → aa; false → cc} - λ{true → bb; false → aa} λ{true → bb; false → bb} λ{true → bb; false → cc} - λ{true → cc; false → aa} λ{true → cc; false → bb} λ{true → cc; false → cc} - -For example, the following function enumerates all possible -arguments of the type `Bool → Tri`: -\begin{code} -→-count : (Bool → Tri) → ℕ -→-count f with f true | f false -... | aa | aa = 1 -... | aa | bb = 2 -... | aa | cc = 3 -... | bb | aa = 4 -... | bb | bb = 5 -... | bb | cc = 6 -... | cc | aa = 7 -... | cc | bb = 8 -... | cc | cc = 9 -\end{code} - -Exponential on types also share a property with exponential on -numbers in that many of the standard identities for numbers carry -over to the types. - -Corresponding to the law - - (p ^ n) ^ m = p ^ (n * m) - -we have the isomorphism - - A → (B → C) ≃ (A × B) → C - -Both types can be viewed as functions that given evidence that `A` holds -and evidence that `B` holds can return evidence that `C` holds. -This isomorphism sometimes goes by the name *currying*. -The proof of the right inverse requires extensionality. -\begin{code} -currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C) -currying = - record - { to = λ{ f → λ{ (x , y) → f x y }} - ; from = λ{ g → λ{ x → λ{ y → g (x , y) }}} - ; from∘to = λ{ f → refl } - ; to∘from = λ{ g → extensionality λ{ (x , y) → refl }} - } -\end{code} - -Currying tells us that instead of a function that takes a pair of arguments, -we can have a function that takes the first argument and returns a function that -expects the second argument. Thus, for instance, our way of writing addition: - - _+_ : ℕ → ℕ → ℕ - -is isomorphic to a function that accepts a pair of arguments: - - _+′_ : (ℕ × ℕ) → ℕ - -Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`. -In a language optimised for pairing, we would take `2 +′ 3` as -an abbreviation for `_+′_ (2 , 3)`. - -Corresponding to the law - - p ^ (n + m) = (p ^ n) * (p ^ m) - -we have the isomorphism - - (A ⊎ B) → C ≃ (A → C) × (B → C) - -That is, the assertion that if either `A` holds or `B` holds then `C` holds -is the same as the assertion that if `A` holds then `C` holds and if -`B` holds then `C` holds. The proof of the left inverse requires extensionality. -\begin{code} -→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C)) -→-distrib-⊎ = - record - { to = λ{ f → ( (λ{ x → f (inj₁ x) }) , (λ{ y → f (inj₂ y) }) ) } - ; from = λ{ (g , h) → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } } - ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } } - ; to∘from = λ{ (g , h) → refl } - } -\end{code} - -Corresponding to the law - - (p * n) ^ m = (p ^ m) * (n ^ m) - -we have the isomorphism - - A → B × C ≃ (A → B) × (A → C) - -That is, the assertion that if either `A` holds then `B` holds and `C` holds -is the same as the assertion that if `A` holds then `B` holds and if -`A` holds then `C` holds. The proof of left inverse requires both extensionality -and the rule `η-×` for products. -\begin{code} -→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C) -→-distrib-× = - record - { to = λ{ f → ( (λ{ x → proj₁ (f x) }) , (λ{ y → proj₂ (f y)}) ) } - ; from = λ{ (g , h) → λ{ x → (g x , h x) } } - ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } } - ; to∘from = λ{ (g , h) → refl } - } -\end{code} - - -## Distribution - -Products distributes over sum, up to isomorphism. The code to validate -this fact is similar in structure to our previous results. -\begin{code} -×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C) -×-distrib-⊎ = - record - { to = λ{ ((inj₁ x) , z) → (inj₁ (x , z)) - ; ((inj₂ y) , z) → (inj₂ (y , z)) - } - ; from = λ{ (inj₁ (x , z)) → ((inj₁ x) , z) - ; (inj₂ (y , z)) → ((inj₂ y) , z) - } - ; from∘to = λ{ ((inj₁ x) , z) → refl - ; ((inj₂ y) , z) → refl - } - ; to∘from = λ{ (inj₁ (x , z)) → refl - ; (inj₂ (y , z)) → refl - } - } -\end{code} - -Sums do not distribute over products up to isomorphism, but it is an embedding. -\begin{code} -⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C) -⊎-distrib-× = - record - { to = λ{ (inj₁ (x , y)) → (inj₁ x , inj₁ y) - ; (inj₂ z) → (inj₂ z , inj₂ z) - } - ; from = λ{ (inj₁ x , inj₁ y) → (inj₁ (x , y)) - ; (inj₁ x , inj₂ z) → (inj₂ z) - ; (inj₂ z , _ ) → (inj₂ z) - } - ; from∘to = λ{ (inj₁ (x , y)) → refl - ; (inj₂ z) → refl - } - } -\end{code} -Note that there is a choice in how we write the `from` function. -As given, it takes `(inj₂ z , inj₂ z′)` to `(inj₂ z)`, but it is -easy to write a variant that instead returns `(inj₂ z′)`. We have -an embedding rather than an isomorphism because the -`from` function must discard either `z` or `z′` in this case. - -In the usual approach to logic, both of the distribution laws -are given as equivalences, where each side implies the other: - - A & (B ∨ C) ⇔ (A & B) ∨ (A & C) - A ∨ (B & C) ⇔ (A ∨ B) & (A ∨ C) - -But when we consider the two laws in terms of evidence, where `_&_` -corresponds to `_×_` and `_∨_` corresponds to `_⊎_`, then the first -gives rise to an isomorphism, while the second only gives rise to an -embedding, revealing a sense in which one of these laws is "more -true" than the other. - - -### Exercise (`×⊎-implies-⊎×`) - -Show that a conjunct of disjuncts implies a disjunct of conjuncts. -\begin{code} -×⊎-Implies-⊎× = ∀ {A B C D : Set} → (A ⊎ B) × (C ⊎ D) → (A × C) ⊎ (B × D) -\end{code} -Does the converse hold? If so, prove; if not, explain why. - - -### Exercise (`⇔-refl`, `⇔-sym`, `⇔-trans`) - -Define equivalence of propositions (also known as "if and only if") as follows. -\begin{code} -record _⇔_ (A B : Set) : Set where - field - to : A → B - from : B → A -\end{code} -Show that equivalence is reflexive, symmetric, and transitive. - - -### Exercise (`⇔-iso`) - -Show that `A ⇔ B` is isomorphic to `(A → B) × (B → A)`. - - -## Standard library - -Definitions similar to those in this chapter can be found in the standard library. -\begin{code} -import Data.Product using (_×_; _,_; proj₁; proj₂) -import Data.Unit using (⊤; tt) -import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to ⊎-elim) -import Data.Empty using (⊥; ⊥-elim) -\end{code} - - -## Unicode - -This chapter uses the following unicode. - - × U+00D7 MULTIPLICATION SIGN (\x) - ⊎ U+228E MULTISET UNION (\u+) - ⊤ U+22A4 DOWN TACK (\top) - ⊥ U+22A5 UP TACK (\bot) - η U+03B7 GREEK SMALL LETTER ETA (\eta) - ₁ U+2081 SUBSCRIPT ONE (\_1) - ₂ U+2082 SUBSCRIPT TWO (\_2) - ⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\<=>) diff --git a/src/Quantifiers-old.lagda b/src/Quantifiers-old.lagda deleted file mode 100644 index 7144d545..00000000 --- a/src/Quantifiers-old.lagda +++ /dev/null @@ -1,394 +0,0 @@ ---- -title : "Quantifiers: Universals and Existentials" -layout : page -permalink : /Quantifiers ---- - -This chapter introduces universal and existential quantification. - -## Imports - -\begin{code} -import Relation.Binary.PropositionalEquality as Eq -open Eq using (_≡_; refl; sym; trans; cong) -open Eq.≡-Reasoning -open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_) -open Isomorphism.≃-Reasoning -open import Data.Nat using (ℕ; zero; suc; _+_; _*_) -open import Data.Nat.Properties.Simple using (+-suc) -open import Relation.Nullary using (¬_) -open import Function using (_∘_) -open import Data.Product using (_×_; _,_; proj₁; proj₂) -open import Data.Sum using (_⊎_; inj₁; inj₂) -\end{code} - -We assume [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 - - -## Universals - -Given a variable `x` of type `A` and a proposition `B x` which -contains `x` as a free variable, the universally quantified -proposition `∀ (x : A) → B x` holds if for every term `M` of type -`A` the proposition `B M` holds. Here `B M` stands for -the proposition `B x` with each free occurrence of `x` replaced by -`M`. The variable `x` appears free in `B x` but bound in -`∀ (x : A) → B x`. We formalise universal quantification using the -dependent function type, which has appeared throughout this book. - -Evidence that `∀ (x : A) → B x` holds is of the form - - λ (x : A) → N - -where `N` is a term of type `B x`, and `N x` and `B x` both contain -a free variable `x` of type `A`. Given a term `L` providing evidence -that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L -M` provides evidence that `B M` holds. In other words, evidence that -`∀ (x : A) → B x` holds is a function that converts a term `M` of type -`A` into evidence that `B M` holds. - -Put another way, if we know that `∀ (x : A) → B x` holds and that `M` -is a term of type `A` then we may conclude that `B M` holds. -\begin{code} -∀-elim : ∀ {A : Set} {B : A → Set} → (∀ (x : A) → B x) → (M : A) → B M -∀-elim L M = L M -\end{code} -As with `→-elim`, the rule corresponds to function application. - -Functions arise as a special case of dependent functions, -where the range does not depend on a variable drawn from the domain. -When a function is viewed as evidence of implication, both its -argument and result are viewed as evidence, whereas when a dependent -function is viewed as evidence of a universal, its argument is viewed -as an element of a data type and its result is viewed as evidence of -a proposition that depends on the argument. This difference is largely -a matter of interpretation, since in Agda values of a type and -evidence of a proposition are indistinguishable. - -Dependent function types are sometimes referred to as dependent products, -because if `A` is a finite type with values `x₁ , ⋯ , xᵢ`, and if -each of the types `B x₁ , ⋯ , B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members, -then `∀ (x : A) → B x` has `m₁ * ⋯ * mᵢ` members. -Indeed, sometimes the notation `∀ (x : A) → B x` -is replaced by a notation such as `Π[ x ∈ A ] (B x)`, -where `Π` stands for product. However, we will stick with the name -dependent function, because (as we will see) dependent product is ambiguous. - - -### Exercise (`∀-distrib-×`) - -Show that universals distribute over conjunction. -\begin{code} -∀-Distrib-× = ∀ {A : Set} {B C : A → Set} → - (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) -\end{code} -Compare this with the result (`→-distrib-×`) in Chapter [Connectives](Connectives). - -### Exercise (`⊎∀-implies-∀⊎`) - -Show that a disjunction of universals implies a universal of disjunctions. -\begin{code} -⊎∀-Implies-∀⊎ = ∀ {A : Set} { B C : A → Set } → - (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x -\end{code} -Does the converse hold? If so, prove; if not, explain why. - - -## Existentials - -Given a variable `x` of type `A` and a proposition `B x` which -contains `x` as a free variable, the existentially quantified -proposition `Σ[ x ∈ A ] B x` holds if for some term `M` of type -`A` the proposition `B M` holds. Here `B M` stands for -the proposition `B x` with each free occurrence of `x` replaced by -`M`. The variable `x` appears free in `B x` but bound in -`Σ[ x ∈ A ] B x`. - -We formalise existential quantification by declaring a suitable -inductive type. -\begin{code} -data Σ (A : Set) (B : A → Set) : Set where - _,_ : (x : A) → B x → Σ A B -\end{code} -We define a convenient syntax for existentials as follows. -\begin{code} -infix 2 Σ-syntax - -Σ-syntax = Σ - -syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B -\end{code} -This is our first use of a syntax declaration, which specifies that -the term on the left may be written with the syntax on the right. -The special syntax is available only when the identifier -`Σ-syntax` is imported. - -Evidence that `Σ[ x ∈ A ] B x` holds is of the form -`(M , N)` where `M` is a term of type `A`, and `N` is evidence -that `B M` holds. - -Equivalently, we could also declare existentials as a record type. -\begin{code} -record Σ′ (A : Set) (B : A → Set) : Set where - field - proj₁′ : A - proj₂′ : B proj₁′ -\end{code} -Here record construction - - record - { proj₁′ = M - ; proj₂′ = N - } - -corresponds to the term - - ( M , N ) - -where `M` is a term of type `A` and `N` is a term of type `B M`. - -Products arise a special case of existentials, where the second -component does not depend on a variable drawn from the first -component. When a product is viewed as evidence of a conjunction, -both of its components are viewed as evidence, whereas when it is -viewed as evidence of an existential, the first component is viewed as -an element of a datatype and the second component is viewed as -evidence of a proposition that depends on the first component. This -difference is largely a matter of interpretation, since in Agda values -of a type and evidence of a proposition are indistinguishable. - -Existentials are sometimes referred to as dependent sums, -because if `A` is a finite type with values `x₁ , ⋯ , xᵢ`, and if -each of the types `B x₁ , ⋯ B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members, -then `Σ[ x ∈ A] B x` has `m₁ + ⋯ + mᵢ` members, which explains the -choice of notation for existentials, since `Σ` stands for sum. - -Existentials are sometimes referred to as dependent products, since -products arise as a special case. However, that choice of names is -doubly confusing, since universal also have a claim to the name dependent -product and since existential also have a claim to the name dependent sum. - -A common notation for existentials is `∃` (analogous to `∀` for universals). -We follow the convention of the Agda standard library, and reserve this -notation for the case where the domain of the bound variable is left implicit. -\begin{code} -∃ : ∀ {A : Set} (B : A → Set) → Set -∃ {A} B = Σ A B - -∃-syntax = ∃ - -syntax ∃-syntax (λ x → B) = ∃[ x ] B -\end{code} -The special syntax is available only when the identifier `∃-syntax` is imported. -We will tend to use this syntax, since it is shorter and more familiar. - -Given evidence that `∀ x → B x → C` holds, where `C` does not contain -`x` as a free variable, and given evidence that `∃[ x ] B x` holds, we -may conclude that `C` holds. -\begin{code} -∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) → ∃[ x ] B x → C -∃-elim f (x , y) = f x y -\end{code} -In other words, if we know for every `x` of type `A` that `B x` -implies `C`, and we know for some `x` of type `A` that `B x` holds, -then we may conclude that `C` holds. This is because we may -instantiate that proof that `∀ x → B x → C` to any value `x` of type -`A` and any `y` of type `B x`, and exactly such values are provided by -the evidence for `∃[ x ] B x`. - -Indeed, the converse also holds, and the two together form an isomorphism. -\begin{code} -∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) ≃ (∃[ x ] B x → C) -∀∃-currying = - record - { to = λ{ f → λ{ (x , y) → f x y }} - ; from = λ{ g → λ{ x → λ{ y → g (x , y) }}} - ; from∘to = λ{ f → refl } - ; to∘from = λ{ g → extensionality λ{ (x , y) → refl }} - } -\end{code} -The result can be viewed as a generalisation of currying. Indeed, the code to -establish the isomorphism is identical to what we wrote when discussing -[implication][implication]. - -[implication]: Connectives/index.html#implication - -### Exercise (`∃-distrib-⊎`) - -Show that universals distribute over conjunction. -\begin{code} -∃-Distrib-⊎ = ∀ {A : Set} {B C : A → Set} → - ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x) -\end{code} - -### Exercise (`∃×-implies-×∃`) - -Show that an existential of conjunctions implies a conjunction of existentials. -\begin{code} -∃×-Implies-×∃ = ∀ {A : Set} { B C : A → Set } → - ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x) -\end{code} -Does the converse hold? If so, prove; if not, explain why. - - -## An existential example - -Recall the definitions of `even` and `odd` from Chapter [Relations](Relations). -\begin{code} -data even : ℕ → Set -data odd : ℕ → Set - -data even where - even-zero : even zero - even-suc : ∀ {n : ℕ} → odd n → even (suc n) - -data odd where - odd-suc : ∀ {n : ℕ} → even n → odd (suc n) -\end{code} -A number is even if it is zero or the successor of an odd number, and -odd if it the successor of an even number. - -We will show that a number is even if and only if it is twice some -other number, and odd if and only if it is one more than twice -some other number. In other words, we will show - - even n iff ∃[ m ] ( m * 2 ≡ n) - odd n iff ∃[ m ] (1 + m * 2 ≡ n) - -By convention, one tends to write constant factors first and to put -the constant term in a sum last. Here we've reversed each of those -conventions, because doing so eases the proof. - -Here is the proof in the forward direction. -\begin{code} -even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] ( m * 2 ≡ n) -odd-∃ : ∀ {n : ℕ} → odd n → ∃[ m ] (1 + m * 2 ≡ n) - -even-∃ even-zero = zero , refl -even-∃ (even-suc o) with odd-∃ o -... | m , refl = suc m , refl - -odd-∃ (odd-suc e) with even-∃ e -... | m , refl = m , refl -\end{code} -We define two mutually recursive functions. Given -evidence that `n` is even or odd, we return a -number `m` and evidence that `m * 2 ≡ n` or `1 + m * 2 ≡ n`. -We induct over the evidence that `n` is even or odd. - -- If the number is even because it is zero, then we return a pair -consisting of zero and the (trivial) proof that twice zero is zero. - -- If the number is even because it is one more than an odd number, -then we apply the induction hypothesis to give a number `m` and -evidence that `1 + m * 2 ≡ n`. We return a pair consisting of `suc m` -and evidence that `suc m * 2` ≡ suc n`, which is immediate after -substituting for `n`. - -- If the number is odd because it is the successor of an even number, -then we apply the induction hypothesis to give a number `m` and -evidence that `m * 2 ≡ n`. We return a pair consisting of `suc m` and -evidence that `1 + 2 * m = suc n`, which is immediate after -substituting for `n`. - -This completes the proof in the forward direction. - -Here is the proof in the reverse direction. -\begin{code} -∃-even : ∀ {n : ℕ} → ∃[ m ] ( m * 2 ≡ n) → even n -∃-odd : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) → odd n - -∃-even ( zero , refl) = even-zero -∃-even (suc m , refl) = even-suc (∃-odd (m , refl)) - -∃-odd ( m , refl) = odd-suc (∃-even (m , refl)) -\end{code} -Given a number that is twice some other number we must show it is -even, and a number that is one more than twice some other number we -must show it is odd. We induct over the evidence of the existential, -and in the even case consider the two possibilities for the number -that is doubled. - -- In the even case for `zero`, we must show `2 * zero` is even, which -follows by `even-zero`. - -- In the even case for `suc n`, we must show `2 * suc m` is even. The -inductive hypothesis tells us that `1 + 2 * m` is odd, from which the -desired result follows by `even-suc`. - -- In the odd case, we must show `1 + m * 2` is odd. The inductive -hypothesis tell us that `m * 2` is even, from which the desired result -follows by `odd-suc`. - -This completes the proof in the backward direction. - -### Exercise (`∃-even′, ∃-odd′`) - -How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2` -by `2 * m` and `2 * m + 1`? Rewrite the proofs of `∃-even` and `∃-odd` when -restated in this way. - - -## Existentials, Universals, and Negation - -Negation of an existential is isomorphic to universal -of a negation. Considering that existentials are generalised -disjunction and universals are generalised conjunction, this -result is analogous to the one which tells us that negation -of a disjunction is isomorphic to a conjunction of negations. -\begin{code} -¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x -¬∃∀ = - record - { to = λ{ ¬∃xy x y → ¬∃xy (x , y) } - ; from = λ{ ∀¬xy (x , y) → ∀¬xy x y } - ; from∘to = λ{ ¬∃xy → extensionality λ{ (x , y) → refl } } - ; to∘from = λ{ ∀¬xy → refl } - } -\end{code} -In the `to` direction, we are given a value `¬∃xy` of type -`¬ ∃[ x ] B x`, and need to show that given a value -`x` that `¬ B x` follows, in other words, from -a value `y` of type `B x` we can derive false. Combining -`x` and `y` gives us a value `(x , y)` of type `∃[ x ] B x`, -and applying `¬∃xy` to that yields a contradiction. - -In the `from` direction, we are given a value `∀¬xy` of type -`∀ x → ¬ B x`, and need to show that from a value `(x , y)` -of type `∃[ x ] B x` we can derive false. Applying `∀¬xy` -to `x` gives a value of type `¬ B x`, and applying that to `y` yields -a contradiction. - -The two inverse proofs are straightforward, where one direction -requires extensionality. - - - -### Exercise (`∃¬-Implies-¬∀`) - -Show `∃[ x ] ¬ B x → ¬ (∀ x → B x)`. - -Does the converse hold? If so, prove; if not, explain why. - - -## Standard Prelude - -Definitions similar to those in this chapter can be found in the standard library. -\begin{code} -import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax) -\end{code} - - -## Unicode - -This chapter uses the following unicode. - - ∃ U+2203 THERE EXISTS (\ex, \exists) - - diff --git a/src/ListsAns.lagda b/src/answers/ListsAns.lagda similarity index 100% rename from src/ListsAns.lagda rename to src/answers/ListsAns.lagda diff --git a/src/NegationAns.lagda b/src/answers/NegationAns.lagda similarity index 100% rename from src/NegationAns.lagda rename to src/answers/NegationAns.lagda diff --git a/src/PropertiesAns.lagda b/src/answers/PropertiesAns.lagda similarity index 100% rename from src/PropertiesAns.lagda rename to src/answers/PropertiesAns.lagda diff --git a/src/RelationsAns.lagda b/src/answers/RelationsAns.lagda similarity index 100% rename from src/RelationsAns.lagda rename to src/answers/RelationsAns.lagda diff --git a/src/extra/Nat.agda b/src/extra/Nat.agda new file mode 100644 index 00000000..c48f04dc --- /dev/null +++ b/src/extra/Nat.agda @@ -0,0 +1,31 @@ +module Nat where + +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl) +open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎) + +data ℕ : Set where + zero : ℕ + suc : ℕ → ℕ + +{-# BUILTIN NATURAL ℕ #-} + +_+_ : ℕ → ℕ → ℕ +zero + n = n +(suc m) + n = suc (m + n) + +_ : 2 + 3 ≡ 5 +_ = + begin + 2 + 3 + ≡⟨⟩ + suc (1 + 3) + ≡⟨⟩ + suc (suc (0 + 3)) + ≡⟨⟩ + suc (suc 3) + ≡⟨⟩ + 5 + ∎ + +