From b60bc9a8d8ded90e302b1f95f22718ac78599939 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 12 Jan 2018 17:20:52 -0200 Subject: [PATCH] Logic, embedding --- src/Logic.lagda | 247 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 166 insertions(+), 81 deletions(-) diff --git a/src/Logic.lagda b/src/Logic.lagda index b58512d2..39e18ffc 100644 --- a/src/Logic.lagda +++ b/src/Logic.lagda @@ -13,7 +13,7 @@ function, dependent product, Martin Löf equivalence). \begin{code} import Relation.Binary.PropositionalEquality as Eq -open Eq using (_≡_; refl; sym; trans; cong) +open Eq using (_≡_; refl; sym; trans; cong; cong-app) open Eq.≡-Reasoning open import Data.Nat using (ℕ) \end{code} @@ -155,6 +155,84 @@ We will make good use of isomorphisms in what follows to demonstrate that operations on types such as product and sum satisfy properties akin to associativity, commutativity, and distributivity. +## Embedding + +We will also need the notion of *embedding*, which is a weakening +of isomorphism. While an isomorphism shows that two types are +in one-to-one correspondence, and embedding shows that the first +type is, in a sense, included in the second; or, equivalently, +that there is a many-to-one correspondence between the second +type and the first. + +Here is the formal definition of embedding. +\begin{code} +record _≲_ (A B : Set) : Set where + field + to : A → B + fro : B → A + invˡ : ∀ (x : A) → fro (to x) ≡ x +open _≲_ +\end{code} +It is the same as an isomorphism, save that it lacks the `invʳ` field. +Hence, we know that `fro` is left inverse to `to`, but not that it is +a right inverse. + +Embedding is reflexive and transitive. The proofs are cut down +versions of the similar proofs for isomorphism, simply dropping the +right inverses. +\begin{code} +≲-refl : ∀ {A : Set} → A ≲ A +≲-refl = + record + { to = λ x → x + ; fro = λ y → y + ; invˡ = λ x → refl + } + +≲-tran : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C +≲-tran A≲B B≲C = + record + { to = λ x → to B≲C (to A≲B x) + ; fro = λ y → fro A≲B (fro B≲C y) + ; invˡ = λ x → + begin + fro A≲B (fro B≲C (to B≲C (to A≲B x))) + ≡⟨ cong (fro A≲B) (invˡ B≲C (to A≲B x)) ⟩ + fro A≲B (to A≲B x) + ≡⟨ invˡ A≲B x ⟩ + x + ∎ + } +\end{code} +It is also easy to see that if two types embed in each other, +and the embedding functions correspond, then they are isomorphic. +This is a weak form of anti-symmetry. +\begin{code} +≲-antisym : ∀ {A B : Set} → (A≲B : A ≲ B) → (B≲A : B ≲ A) → + (to A≲B ≡ fro B≲A) → (fro A≲B ≡ to B≲A) → A ≃ B +≲-antisym A≲B B≲A to≡fro fro≡to = + record + { to = to A≲B + ; fro = fro A≲B + ; invˡ = invˡ A≲B + ; invʳ = λ y → + begin + to A≲B (fro A≲B y) + ≡⟨ cong (\w → to A≲B (w y)) fro≡to ⟩ + to A≲B (to B≲A y) + ≡⟨ cong (\w → w (to B≲A y)) to≡fro ⟩ + fro B≲A (to B≲A y) + ≡⟨ invˡ B≲A y ⟩ + y + ∎ + } +\end{code} +The first three components are copied from the embedding, while the +last combines the left inverse of `B ≲ A` with the equivalences of +the `to` and `fro` components from the two embeddings to obtain +the right inverse of the isomorphism. + + @@ -184,7 +262,7 @@ snd (x , y) = y If `w` is evidence that `A × B` holds, then `fst w` is evidence that `A` holds, and `snd w` is evidence that `B` holds. -Equivalently, we could also declare products as a record type. +Equivalently, we could also declare product as a record type. \begin{code} record _×′_ (A B : Set) : Set where field @@ -219,11 +297,12 @@ Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and 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*. Among other reasons for +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 three members, and +For instance, consider a type `Bool` with two members, and a type `Tri` with three members. \begin{code} data Bool : Set where @@ -257,11 +336,11 @@ 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 `fro` function does the inverse -(which also swaps a pair). Replacing `invˡ` -or `invʳ` by `λ w → refl` will not work. +For commutativity, the `to` function swaps a pair, taking `(x , y)` to +`(y , x)`, and the `fro` function does the same (up to renaming). +Instantiating the patterns correctly in `invˡ` and `invʳ` is essential. +Replacing the definition of `invˡ` by `λ w → refl` will not work; +and similarly for `invʳ`, which does the same (up to renaming). \begin{code} ×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A) ×-comm = record @@ -280,12 +359,12 @@ isomorphism*. Compare the two statements: 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---a -one-to-one correspondence---between the two types. For +*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 a pair of pairs, +For associativity, the `to` function reassociates two uses of pairing, taking `((x , y) , z)` to `(x , (y , z))`, and the `fro` function does the inverse. Again, the evidence of left and right inverse requires matching against a suitable pattern to enable simplificition. @@ -303,7 +382,7 @@ 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 `((1 , true) , aa)`, -which is a member of the former, corresponds to `(1 , (true , aa)`, +which is a member of the former, corresponds to `(1 , (true , aa))`, which is a member of the latter. Here we have used lambda-expressions with pattern matching. @@ -319,8 +398,8 @@ h (x , y) = (y , x) Often using an anonymous lambda expression is more convenient than using a named function: it avoids a lengthy type declaration; and the definition appears exactly where the function is used, so there is no -need for the writer to remember to declare it in advance, or the reader -to search for the definition elsewhere in the code. +need for the writer to remember to declare it in advance, or for the +reader to search for the definition elsewhere in the code. ## Disjunction is sum @@ -356,7 +435,8 @@ 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*. Among other reasons for +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. @@ -379,102 +459,107 @@ possible arguments of type `Bool ⊎ Tri`: ⊎-count (inj₂ cc) = 5 \end{code} -Sum on types also shares a property with sum 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*. +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 a pair, -taking `(x , y)` to `(y , x)`, and -the `fro` function does the inverse -(which also swaps a pair). Replacing `invˡ` -or `invʳ` by `λ w → refl` will not work. +For commutativity, the `to` function swaps the two constructors, +taking `inj₁ x` to `inj₂ x`, and `inj₂ y` to `inj₁ y`; and the `fro` +function does the same (up to renaming). Replacing the definition of +`invˡ` by `λ w → refl` will not work; and similarly for `invʳ`, which +does the same (up to renaming). \begin{code} -{- -×-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 } ++-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 + } } --} \end{code} Being *commutative* is different from being *commutative up to isomorphism*. Compare the two statements: - m * n ≡ n * m - A × B ≃ B × A + 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---a -one-to-one correspondence---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. +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 a pair of pairs, -taking `((x , y) , z)` to `(x , (y , z))`, and the `fro` function does +For associativity, the `to` function reassociates, and the `fro` function does the inverse. Again, the evidence of left and right inverse requires matching against a suitable pattern to enable simplificition. \begin{code} -{- -×-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 } ++-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)) + } + ; fro = λ { (inj₁ x) → (inj₁ (inj₁ x)) + ; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y)) + ; (inj₂ (inj₂ z)) → (inj₂ z) + } + ; invˡ = λ { (inj₁ (inj₁ x)) → refl + ; (inj₁ (inj₂ y)) → refl + ; (inj₂ z) → refl + } + ; invʳ = λ { (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 `((1 , true) , aa)`, -which is a member of the former, corresponds to `(1 , (true , aa)`, +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. -Here we have used lambda-expressions with pattern matching. -For instance, the term +Here we have used lambda-expressions with pattern matching +and multiple cases. For instance, the term - λ { (x , y) → (y , x) } + λ { (inj₁ x) → (inj₂ x) + ; (inj₂ y) → (inj₁ y) + } -corresponds to the function `h`, where `h` is defined by +corresponds to the function `k`, where `k` is defined by \begin{code} -{- -h : ∀ {A B : Set} → A × B → B × A -h (x , y) = (y , x) --} +k : ∀ {A B : Set} → A ⊎ B → B ⊎ A +k (inj₁ x) = inj₂ x +k (inj₂ y) = inj₁ y \end{code} -Often using an anonymous lambda expression is more convenient than -using a named function: it avoids a lengthy type declaration; and the -definition appears exactly where the function is used, so there is no -need for the writer to remember to declare it in advance, or the reader -to search for the definition elsewhere in the code. - ## Distribution Distribution of `×` over `⊎` is an isomorphism. \begin{code} -{- -×-distributes-+ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C)) -×-distributes-+ = +×-distributes-⊎ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C)) +×-distributes-⊎ = record { - to = λ { (inj₁ a , c) → (inj₁ (a , c)) ; - (inj₂ b , c) → (inj₂ (b , c)) } ; - fro = λ { (inj₁ (a , c)) → (inj₁ a , c) ; - (inj₂ (b , c)) → (inj₂ b , c) } ; - invˡ = λ { (inj₁ a , c) → refl ; - (inj₂ b , c) → refl } ; - invʳ = λ { (inj₁ (a , c)) → refl ; - (inj₂ (b , c)) → refl } + to = λ { ((inj₁ x) , z) → (inj₁ (x , z)) ; + ((inj₂ y) , z) → (inj₂ (y , z)) } ; + fro = λ { (inj₁ (x , z)) → ((inj₁ x) , z) ; + (inj₂ (y , z)) → ((inj₂ y) , z) } ; + invˡ = λ { ((inj₁ x) , z) → refl ; + ((inj₂ y) , z) → refl } ; + invʳ = λ { (inj₁ (x , z)) → refl ; + (inj₂ (y , z)) → refl } } --} \end{code} Distribution of `⊎` over `×` is half an isomorphism.