From dffb291510ecfa69f1de7f9bf1dfa1e9d30eddb4 Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 12 Mar 2018 12:53:30 -0300 Subject: [PATCH] completed pass over Equality --- src/Equality.lagda | 148 +++++++++++++++++++++++++-------------------- src/Naturals.lagda | 20 +----- 2 files changed, 84 insertions(+), 84 deletions(-) diff --git a/src/Equality.lagda b/src/Equality.lagda index 1bdf4ab5..e99acc46 100644 --- a/src/Equality.lagda +++ b/src/Equality.lagda @@ -4,9 +4,6 @@ layout : page permalink : /Equality --- - - Much of our reasoning has involved equality. Given two terms `M` and `N`, both of type `A`, we write `M ≡ N` to assert that `M` and `N` are interchangeable. So far we have taken equivalence as a primitive, @@ -31,8 +28,8 @@ open import Agda.Primitive using (Level; lzero; lsuc) We declare equivality as follows. \begin{code} -data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where - refl : x ≡ x +data _≡_ {A : Set} : A → A → Set where + refl : ∀ {x : A} → x ≡ x \end{code} In other words, for any type `A` and for any `x` of type `A`, the constructor `refl` provides evidence that `x ≡ x`. Hence, every value @@ -61,7 +58,7 @@ An equivalence relation is one which is reflexive, symmetric, and transitive. Reflexivity is built-in to the definition of equivalence, via the constructor `refl`. It is straightforward to show symmetry. \begin{code} -sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x +sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x sym refl = refl \end{code} How does this proof work? The argument to `sym` has type `x ≡ y`, @@ -112,7 +109,7 @@ This completes the definition as given above. Transitivity is equally straightforward. \begin{code} -trans : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z +trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z trans refl refl = refl \end{code} Again, a useful exercise is to carry out an interactive development, checking @@ -121,14 +118,14 @@ instantiated. ## Congruence and Substitution -Equality also satisfies *congruence*. If two terms are equal, +Equality satisfies *congruence*. If two terms are equal, they remain so after the same function is applied to both. \begin{code} -cong : ∀ {ℓ} {A B : Set ℓ} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y +cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y cong f refl = refl \end{code} -Once more, a useful exercise is to carry out an interactive development. +Equality also satisfies *substitution*. If two values are equal and a predicate holds of the first then it also holds of the second. \begin{code} subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y @@ -136,14 +133,14 @@ subst P refl px = px \end{code} -## Tabular reasoning +## Chains of equations -Here we show how to support the form of tabular reasoning -we have used throughout the book. We package the declarations +Here we show how to support reasoning with chains of equations +as used throughout the book. We package the declarations into a module, named `≡-Reasoning`, to match the format used in Agda's standard library. \begin{code} -module ≡-Reasoning {ℓ} {A : Set ℓ} where +module ≡-Reasoning {A : Set} where infix 1 begin_ infixr 2 _≡⟨⟩_ _≡⟨_⟩_ @@ -166,11 +163,11 @@ open ≡-Reasoning Opening the module makes all of the definitions available in the current environment. -As a simple example, let's look at the proof of transitivity -rewritten in tabular form. +As an example, let's look at a proof of transitivity +as a chain of equations. \begin{code} -trans′ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z -trans′ {ℓ} {A} {x} {y} {z} x≡y y≡z = +trans′ : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z +trans′ {A} {x} {y} {z} x≡y y≡z = begin x ≡⟨ x≡y ⟩ @@ -179,7 +176,7 @@ trans′ {ℓ} {A} {x} {y} {z} x≡y y≡z = z ∎ \end{code} -According to the fixity declarations, the body parses as follows. +According to the fixity declarations, the body parses as follows: begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎))) @@ -195,21 +192,20 @@ third arguments are both proofs of equations, in particular proofs of `y ≡ z` and `z ≡ z` respectively, which are combined by `trans` in the body of `_≡⟨_⟩_` to yield a proof of `y ≡ z`. Finally, the proof of `z ≡ z` consists of `_∎` applied to the term `z`, which yields `refl`. -After simplification, the body is equivalent to the following term. +After simplification, the body is equivalent to the term: trans x≡y (trans y≡z refl) We could replace all uses of tabular reasoning by a chain of -applications of `trans`; the result would be more compact but harder to read. -Also note that the syntactic trick behind `∎` means that the chain -always ends in the form `trans e refl`, where `e` proves some equation, -even though `e` alone would do. +applications of `trans`; the result would be more compact but harder +to read. The trick behind `∎` means that the chain always ends in the +form `trans e refl`, where `e` proves some equation, even though `e` +alone would do. - ## Rewriting Consider a property of natural numbers, such as being even. - +We repeat the earlier definition. \begin{code} -data even : ℕ → Set where - ev0 : even zero - ev+2 : ∀ {n : ℕ} → even n → even (suc (suc n)) +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} In the previous section, we proved addition is commutative. Given evidence that `even (m + n)` holds, @@ -303,9 +302,6 @@ corresponds to equivalence. We can then prove the desired property as follows. \begin{code} -postulate - +-comm : ∀ (m n : ℕ) → m + n ≡ n + m - even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m) even-comm m n ev rewrite +-comm m n = ev \end{code} @@ -375,16 +371,24 @@ even-comm′ m n ev with m + n | +-comm m n \end{code} The first clause asserts that `m + n` and `n + m` are identical, and the second clause justifies that assertion with evidence of the -appropriate equivalence. Note the use of the "dot pattern" `.(n + -m)`. A dot pattern is followed by an expression and is made when -other information allows one to identify the expession in the `with` -clause with the expression it matches against. In this case, the -identification of `m + n` and `n + m` is justified by the subsequent -matching of `+-comm m n` against `refl`. One might think that the -first clause is redundant as the information is inherent in the second -clause, but in fact Agda is rather picky on this point: omitting the -first clause or reversing the order of the clauses will cause Agda to -report an error. (Try it and see!) +appropriate equivalence. Note the use of the "dot pattern", `.(n + m)`. +A dot pattern is followed by an expression and is made when +other information forces the value matched to be equal to the value of +the expression in the dot pattern. In this case, the identification +of `m + n` and `n + m` is justified by the subsequent matching of +`+-comm m n` against `refl`. One might think that the first clause is +redundant as the information is inherent in the second clause, but in +fact Agda is rather picky on this point: omitting the first clause or +reversing the order of the clauses will cause Agda to report an error. +(Try it and see!) + +In this case, we can avoid rewrite by simply applying substitution. +\begin{code} +even-comm″ : ∀ (m n : ℕ) → even (m + n) → even (n + m) +even-comm″ m n = subst even (+-comm m n) +\end{code} +Nonetheless, rewrite is a vital part of the Agda toolkit, +as earlier examples have shown. ## Leibniz equality @@ -407,20 +411,32 @@ holds of `y` also holds of `x`. Let `x` and `y` be objects of type $A$. We say that `x ≐ y` holds if for every predicate $P$ over type $A$ we have that `P x` implies `P y`. \begin{code} -_≐_ : ∀ {ℓ} {A : Set ℓ} (x y : A) → Set (lsuc ℓ) -_≐_ {ℓ} {A} x y = (P : A → Set ℓ) → P x → P y +_≐_ : ∀ {A : Set} (x y : A) → Set₁ +_≐_ {A} x y = ∀ (P : A → Set) → P x → P y \end{code} -Here we must make use of levels: if `A` is a set at level `ℓ` and `x` and `y` -are two values of type `A` then `x ≐ y` is at the next level `lsuc ℓ`. +One might expect to write the left-hand side of the equation as `x ≐ y`, +but instead we write `_≐_ {A} x y` to provide access to the implicit +parameter `A` which appears on the right-hand side. + +This is our first use of *levels*. We cannot assign `Set` the type +`Set`, since this would lead to contradictions such as Russel's +Paradox and Girard's Paradox. Instead, there is a hierarchy of types, +where `Set : Set₁`, `Set₁ : Set₂`, and so on. In fact, `Set` itself +is just an abbreviation for `Set₀`. Since the equation defining `_≐_` +mentions `Set` on the right-hand side, the corresponding signature +must use `Set₁`. Further information on levels can be found in +the [Agda Wiki][wiki]. + +[wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism Leibniz equality is reflexive and transitive, where the first follows by a variant of the identity function and the second by a variant of function composition. \begin{code} -refl-≐ : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≐ x +refl-≐ : ∀ {A : Set} {x : A} → x ≐ x refl-≐ P Px = Px -trans-≐ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≐ y → y ≐ z → x ≐ z +trans-≐ : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z → x ≐ z trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px) \end{code} @@ -433,10 +449,10 @@ implies `P x`. The property `Q x` is trivial by reflexivity, and hence `Q y` follows from `x ≐ y`. But `Q y` is exactly a proof of what we require, that `P y` implies `P x`. \begin{code} -sym-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → y ≐ x -sym-≐ {ℓ} {A} {x} {y} x≐y P = Qy +sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x +sym-≐ {A} {x} {y} x≐y P = Qy where - Q : A → Set ℓ + Q : A → Set Q z = P z → P x Qx : Q x Qx = refl-≐ P @@ -450,24 +466,22 @@ Leibniz equality, and vice versa. In the forward direction, if we know which is easy since equivalence of `x` and `y` implies that any proof of `P x` is also a proof of `P y`. \begin{code} -≡-implies-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x ≐ y -≡-implies-≐ refl P Px = Px +≡-implies-≐ : ∀ {A : Set} {x y : A} → x ≡ y → x ≐ y +≡-implies-≐ x≡y P = subst P x≡y \end{code} -The function `≡-implies-≐` is often called *substitution* because it -says that if we know `x ≡ y` then we can substitute `y` for `x`, -taking a proof of `P x` to a proof of `P y` for any property `P`. +This direction follows from substitution, which we showed earlier. In the reverse direction, given that for any `P` we can take a proof of `P x` to a proof of `P y` we need to show `x ≡ y`. The proof is similar to that -for symmetry of Leibniz equality. We take $Q$ +for symmetry of Leibniz equality. We take `Q` to be the predicate that holds of `z` if `x ≡ z`. Then `Q x` is trivial by reflexivity of Martin Löf equivalence, and hence `Q y` follows from `x ≐ y`. But `Q y` is exactly a proof of what we require, that `x ≡ y`. \begin{code} -≐-implies-≡ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → x ≡ y -≐-implies-≡ {ℓ} {A} {x} {y} x≐y = Qy +≐-implies-≡ : ∀ {A : Set} {x y : A} → x ≐ y → x ≡ y +≐-implies-≡ {A} {x} {y} x≐y = Qy where - Q : A → Set ℓ + Q : A → Set Q z = x ≡ z Qx : Q x Qx = refl diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 34d9e36f..ba7a6acd 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -393,24 +393,10 @@ check it is the same as `5`. A binary relation is said to be *reflexive* if it holds between a value and itself. Evidence that a value is equal to itself is written `refl`. -In the chains of equations, all Agda checks is that each of the terms +In the chains of equations, all Agda checks is that each term simplifies to the same value. If we jumble the equations, omit lines, or -add extraneous lines it will still be accepted. -\begin{code} -_ : 2 + 3 ≡ 5 -_ = - begin - 2 + 3 - ≡⟨⟩ - 4 + 1 - ≡⟨⟩ - 5 - ≡⟨⟩ - suc (suc (0 + 3)) - ∎ -\end{code} -Of course, writing a proof in this way would be misleading and confusing, -so it's to be avoided even if Agda does accept it. +add extraneous lines it will still be accepted. It's up to us to write +the equations in an order that makes sense to the reader. Here `2 + 3 ≡ 5` is a type, and the chains of equations (and also `refl`) are terms of the given type; alternatively, one can think of