From f1d49466133590745525cfb7cbddd1ec45f4eb79 Mon Sep 17 00:00:00 2001 From: wadler Date: Thu, 4 Jan 2018 13:23:15 -0200 Subject: [PATCH] starting on antisymmetry --- src/Relations.lagda | 115 +++++++++++++++++++++++++++++++++----------- 1 file changed, 88 insertions(+), 27 deletions(-) diff --git a/src/Relations.lagda b/src/Relations.lagda index 1181b468..480d99c9 100644 --- a/src/Relations.lagda +++ b/src/Relations.lagda @@ -116,9 +116,44 @@ tightly that `_+_` at level 6, or `_*_` at level 7. infix 4 _≤_ \end{code} -## Reflexivity and transitivity +## Properties of ordering relations -The first thing to prove about comparison is that it is *reflexive*: +Relations occur all the time, and mathematicians have agreed +on names for some of the most common properties. + ++ *Reflexive* For all `n`, the relation `n ≤ n` holds. ++ *Transitive* For all `m`, `n`, and `p`, if `m ≤ n` and +`n ≤ p` hold, then `m ≤ p` holds. ++ *Anti-symmetric* For all `m` and `n`, if both `m ≤ n` and +`n ≤ m` hold, then `m ≡ n` holds. ++ *Total* For all `m` and `n`, either `m ≤ n` or `n ≤ m` +holds. + +The relation `_≤_` satisfies all four of these properties. + +There are also names for some combinations of these properties. + ++ *Preorder* Any relation that is reflexive and transitive. ++ *Partial order* Any preorder that is also anti-symmetric. ++ *Total order* Any partial order that is also total. + +If you ever bump into a relation at a party, you now know how +to make small talk, by asking it whether it is reflexive, transitive, +anti-symmetric, and total. Or instead you might ask whether it is a +preorder, partial order, or total order. + +Less frivolously, if you ever bump into a relation while reading +a technical paper, this gives you an easy way to orient yourself, +by checking whether or not it is a preorder, partial order, or total order. +A careful author will often make it explicit, for instance by saying +that a given relation is a preoder but not a partial order, or a +partial order but not a total order. (Can you think of examples of +such relations?) + + +## Reflexivity + +The first property to prove about comparison is that it is reflexive: for any natural `n`, the relation `n ≤ n` holds. \begin{code} refl≤ : ∀ (n : ℕ) → n ≤ n @@ -128,12 +163,17 @@ refl≤ (suc n) = s≤s (refl≤ n) The proof is a straightforward induction on `n`. In the base case, `zero ≤ zero` holds by `z≤n`. In the inductive case, the inductive hypothesis `refl≤ n` gives us a proof of `n ≤ n`, and applying `s≤s` -to that yields a proof of `suc n ≤ suc n`. It is a good exercise to -create this proof interactively in Emacs, using holes and the `^C ^C`, -`^C ^,`, and `^C ^R` commands. +to that yields a proof of `suc n ≤ suc n`. -The second thing to prove about comparison is that it is *transitive*: -for any naturals `m`, `n`, and `p`, if `m ≤ n` and `n ≤ p` then `m ≤ p`. +It is a good exercise to prove reflexivity interactively in Emacs, +using holes and the `^C ^C`, `^C ^,`, and `^C ^R` commands. + + +## Transitivity + +The second property to prove about comparison is that it is +transitive: for any naturals `m`, `n`, andl `p`, if `m ≤ n` and `n ≤ +p` hold, then `m ≤ p` holds. \begin{code} trans≤ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p trans≤ z≤n _ = z≤n @@ -142,24 +182,25 @@ trans≤ (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤ m≤n n≤p) Here the proof is most easily thought of as by induction on the *evidence* that `m ≤ n`, so we have left `m`, `n`, and `p` implicit. -In the base case, `m ≤ n` holds by `z≤n`, so it must be the case that +In the base case, `m ≤ n` holds by `z≤n`, so it must be that `m` is `zero`, in which case `m ≤ p` also holds by `z≤n`. In this case, the fact that `n ≤ p` is irrelevant, and we write `_` as the pattern to indicate that the corresponding evidence is unused. We could instead have written `n≤p` but not used that variable on the right-hand side of the equation. -In the inductive case, `m ≤ n` holds by `s≤s m≤n`, meaning that `m` -must be of the form `suc m′` and `n` of the form `suc n′` and `m≤n` is +In the inductive case, `m ≤ n` holds by `s≤s m≤n`, so it must be that `m` +is of the form `suc m′` and `n` is of the form `suc n′` and `m≤n` is evidence that `m′ ≤ n′`. In this case, the only way that `p ≤ n` can hold is by `s≤s n≤p`, where `p` is of the form `suc p′` and `n≤p` is evidence that `n′ ≤ p′`. The inductive hypothesis `trans≤ m≤n n≤p` provides evidence that `m′ ≤ p′`, and applying `s≤s` to that gives evidence of the desired conclusion, `suc m′ ≤ suc p′`. -Agda knows that the case `trans≤ (s≤s m≤n) z≤n` cannot arise, since -the first piece of evidence implies `n` must be `suc n′` for some `n′` -while the second implies `n` must be `zero`. +The case `trans≤ (s≤s m≤n) z≤n` cannot arise, since the first piece of +evidence implies `n` must be `suc n′` for some `n′` while the second +implies `n` must be `zero`. Agda can determine that such a case cannot +arise, and does not require it to be listed. Alternatively, we could make the implicit parameters explicit. \begin{code} @@ -169,32 +210,52 @@ trans≤′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (trans \end{code} One might argue that this is clearer, since it shows us the forms of `m`, `n`, and `p`, or one might argue that the extra length obscures the essence of the -proof. We will usually opt for shorter proofs. +proof. We will usually opt for shorter proofs. + +The technique of inducting on evidence that a property holds (e.g., +inducting on evidence that `m ≤ n`)---rather than induction on the +value of which the property holds (e.g., inducting on `m`)---will turn +out to be immensely valuable, and one that we use often. + +Again, it is a good exercise to prove transitivity interactively in Emacs, +using holes and the `^C ^C`, `^C ^,`, and `^C ^R` commands. + +## Antisymmetry + +The third thing to prove about comparison is that it is antisymmetric: +for all naturals `m` and `n`, if both `m ≤ n` and `n ≤ m` hold, then +`m ≡ n` holds. +\begin{code} +antisym≤ : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n +antisym≤ z≤n z≤n = refl +antisym≤ (s≤s m≤n) (s≤s n≤m) rewrite antisym≤ m≤n n≤m = refl +\end{code} +Again, the proof is by induction over the evidence that `m ≤ n` +and `n ≤ m` hold, and so we have left `m` and `n` implicit. + +In the base case, both relations hold by `z≤n`, +so it must be the case that both `m` and `n` are `zero`, +in which case `m ≡ n` holds by reflexivity. (The reflexivity +of equivlance, that is, not the reflexivity of comparison.) + +In the inductive case, `m ≤ n` holds by `s≤s m≤n` and `n ≤ m` +holds by `s≤s n≤m`, -The technique of inducting on evidence that a property holds---rather than -induction on the value of which the property holds---will turn out to be -immensely valuable, and one that we use often. Any ordering relation that is both reflexive and transitive is called -a *partial order*, hence we have shown that "less than or equal" is a -partial order. We will later show that it satisfies a stronger -property, and is also a total order. +a *preorder*, and any preorder that is also antisymmetric is a *partial order*. +Hence, we have shown that "less than or equal" is a partial order. We will +later show that it satisfies the strong property of being a *total order*. +## Monotonicity -can equally be regarded as by induction on `m` or by induction -on the evidence that `m ≤ n`. If `m - \begin{code} -antisym≤ : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n -antisym≤ z≤n z≤n = refl -antisym≤ (s≤s m≤n) (s≤s n≤m) rewrite antisym≤ m≤n n≤m = refl - mono+≤ : ∀ (m p q : ℕ) → p ≤ q → m + p ≤ m + q mono+≤ zero p q p≤q = p≤q mono+≤ (suc m) p q p≤q = s≤s (mono+≤ m p q p≤q)