text for reflexivity and transitivity

src/Relations.lagda

@@ -96,27 +96,101 @@ here will write `z≤n` for the proof that `m ≤ m`, leaving the `m` implicit,
 or if `m≤n` is evidence that `m ≤ n`, we write write `s≤s m≤n` for the
 evidence that `suc m ≤ suc n`, leaving both `m` and `n` implicit.
 
-It is possible to provide implicit arguments explicitly if we wish.
+It is possible to provide implicit arguments explicitly if we wish, by
-For instance, here is the Agda proof that `2 ≤ 4` repeated, with the
+writing the arguments inside curly braces.  For instance, here is the
-implicit arguments made explicit.
+Agda proof that `2 ≤ 4` repeated, with the implicit arguments made
+explicit.
 \begin{code}
 ex₂ : 2 ≤ 4
 ex₂ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))
 \end{code}
 
-## Proving properties of inductive definitions.
+## Precedence
 
+We write `infix` to indicate that it is a parse error to write two
+adjacent comparisons, as it makes no sense to give `2 ≤ 4 ≤ 6` either
+the meaning `(2 ≤ 4) ≤ 6` or `(2 ≤ 4) ≤ 6`.The Agda standard library
+sets the precedence of `_≤_` at level 4, which means it binds less
+tightly that `_+_` at level 6, or `_*_` at level 7.
 \begin{code}
 infix 4 _≤_
+\end{code}
 
+## Reflexivity and transitivity
+
+The first thing to prove about comparison is that it is *reflexive*:
+for any natural `n`, the relation `n ≤ n` holds.
+\begin{code}
 refl≤ : ∀ (n : ℕ) → n ≤ n
 refl≤ zero = z≤n
 refl≤ (suc n) = s≤s (refl≤ n)
+\end{code}
+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. 
 
+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`.
+\begin{code}
 trans≤ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
-trans≤ z≤n n≤p = z≤n
+trans≤ z≤n _ = z≤n
 trans≤ (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤ m≤n n≤p)
+\end{code}
+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
+`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
+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`.
+
+Alternatively, we could make the implicit parameters explicit.
+\begin{code}
+trans≤′ : ∀ (m n p : ℕ) → m ≤ n → n ≤ p → m ≤ p
+trans≤′ zero n p z≤n _ = z≤n
+trans≤′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤′ m n p m≤n n≤p)
+\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.
+
+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.
+
+
+
+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
@@ -129,7 +203,7 @@ mono+≤′ : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p
 mono+≤′ m n p m≤n rewrite com+ m p | com+ n p = mono+≤ p m n m≤n
 
 mono+≤″ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m + p ≤ n + q
-mono+≤″ m n p q m≤n p≤q = trans≤ (mono+≤′ m n p m≤n) (mono+≤ n p q p≤q)
+mono+≤″ m n p q m≤n p≤q = trans≤′ (mono+≤′ m n p m≤n) (mono+≤ n p q p≤q)
 
 inverse+∸≤ : ∀ (m n : ℕ) → m ≤ n → (n ∸ m) + m ≡ n
 inverse+∸≤ zero n z≤n rewrite com+zero n  = refl
@@ -142,11 +216,37 @@ data _<_ : ℕ → ℕ → Set where
 
 infix 4 _<_
 
-<implies≤ : ∀ (m n : ℕ) → m < n → suc m ≤ n
+<implies≤ : ∀ {m n : ℕ} → m < n → suc m ≤ n
-<implies≤ m n m<n = ?
+<implies≤ z<s = s≤s z≤n
+<implies≤ (s<s m<n) = s≤s (<implies≤ m<n)
+
+≤implies< : ∀ {m n : ℕ} → suc m ≤ n → m < n
+≤implies< (s≤s z≤n) = z<s
+≤implies< (s≤s (s≤s m≤n)) = s<s (≤implies< (s≤s m≤n))
+\end{code}
+
+## Trichotomy
+
+\begin{code}
+_>_ : ℕ → ℕ → Set
+n > m = m < n
+
+infix 4 _>_
+
+data Trichotomy : ℕ → ℕ → Set where
+  less : ∀ {m n : ℕ} → m < n → Trichotomy m n
+  same : ∀ {m n : ℕ} → m ≡ n → Trichotomy m n
+  more : ∀ {m n : ℕ} → m > n → Trichotomy m n
+
+trichotomy : ∀ (m n : ℕ) → Trichotomy m n
+trichotomy zero zero = same refl
+trichotomy zero (suc n) = less z<s
+trichotomy (suc m) zero = more z<s
+trichotomy (suc m) (suc n) with trichotomy m n
+... | less m<n = less (s<s m<n)
+... | same refl = same refl
+... | more n<m = more (s<s n<m)
 
-≤implies< : ∀ (m n : ℕ) → suc m ≤ n → m < n
-≤implies< m n m≤n = ?
 \end{code}
 
 ## Unicode