starting on antisymmetry

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)