This time I prove the antisymmetry of the order relation, \( a \le b \to b \le a \to a = b \). Trying to prove this directly didn't go anywhere at first, so I first put together two supporting facts: a transitivity law that mixes strict and non-strict order, and irreflexivity of the strict order. With those in place, the main proof becomes much more manageable.
Transitivity across mixed strict and non-strict order
I had already proven ordinary transitivity, deriving \( n < k \) from \( n < m \) and \( m < k \). What I hadn't covered yet were the mixed cases, such as deriving \( n < k \) from \( n \le m \) and \( m < k \). To be able to freely chain \( \le \) and \( < \) inside a calc block, a transitivity lemma is needed for each combination.
variable {n m k : MyNat}
theorem MyNat.lt_trans (h1 : n < m) (h2 : m < k) : n < k := by
notation_simp at *
-- h1 : n + 1 ≤ m
-- h2 : m + 1 ≤ k
-- ⊢ n + 1 ≤ k
have : n + 1 ≤ k := calc
_ ≤ m := by exact h1
_ ≤ m + 1 := by simp
_ ≤ k := by exact h2
assumption
theorem MyNat.lt_of_le_of_lt (h1 : n ≤ m) (h2 : m < k) : n < k := by
notation_simp at *
-- h1 : n ≤ m
-- h2 : m + 1 ≤ k
-- ⊢ n + 1 ≤ k
have : n + 1 ≤ k := calc
_ ≤ m + 1 := by compatible
_ ≤ k := by exact h2
assumption
theorem MyNat.lt_of_lt_of_le (h1 : n < m) (h2 : m ≤ k) : n < k := by
notation_simp at *
-- h2 : m ≤ k
-- h1 : n + 1 ≤ m
-- ⊢ n + 1 ≤ k
have : n + 1 ≤ k := calc
_ ≤ m := by exact h1
_ ≤ k := by exact h2
assumption
instance : Trans (· < · : MyNat → MyNat → Prop) (· < ·) (· < ·) where
trans := MyNat.lt_trans
instance : Trans (· ≤ · : MyNat → MyNat → Prop) (· < ·) (· < ·) where
trans := MyNat.lt_of_le_of_lt
instance : Trans (· < · : MyNat → MyNat → Prop) (· ≤ ·) (· < ·) where
trans := MyNat.lt_of_lt_of_leIn lt_trans, notation_simp unfolds \( < \) into its \( \le \) definition, so the goal becomes \( n + 1 \le k \). Inserting the one-step gap \( m \le m + 1 \) lets me connect h1 : n + 1 \le m and h2 : m + 1 \le k. lt_of_le_of_lt and lt_of_lt_of_le follow the same idea, shifting one of the hypotheses by one step before composing the rest.
Registering these three as Trans instances then lets me freely mix \( \le \) and \( < \) inside calc blocks going forward.
Irreflexivity of the strict order
Irreflexivity means that no element relates to itself. For the strict order, that means \( n < n \) never holds for any \( n \). This turns out to be the key to the antisymmetry proof below, since the strategy there is to derive the contradictory statement \( n < n \) and close the goal with it.
@[simp]
theorem MyNat.lt_irrefl (n : MyNat) : ¬ n < n := by
intro h
notation_simp at h
rw [MyNat.le_iff_add] at *
obtain ⟨k, hk⟩ := h
-- hk : n + 1 + k = n ⊢ False
have : n + (k + 1) = n := calc
_ = n + 1 + k := by ac_rfl
_ = n := by rw [hk]
simp_allAfter introducing the assumption n < n, notation_simp turns it into \( n + 1 \le n \), and MyNat.le_iff_add rewrites that into \( \exists k,\ n + 1 + k = n \). Using the resulting hk, I build \( n + (k + 1) = n \), which by the same mechanism as MyNat.add_right_cancel amounts to \( k + 1 = 0 \) — and simp_all closes the goal from the fact that \( k + 1 = 0 \) never holds.
Antisymmetry of the order
With those two supporting lemmas ready, I can now prove the main theorem: antisymmetry, \( n \le m \to m \le n \to n = m \).
theorem MyNat.le_antisymm (h1: n ≤ m) (h2: m ≤ n) : n = m := by
induction h1 with
| refl => rfl
| @step m h ih =>
-- h : n ≤ m
-- ih : m ≤ n → n = m
-- h2 : m + 1 ≤ n
-- ⊢ n = m + 1
have : n < n := calc
_ ≤ m := by exact h
_ < m + 1 := by notation_simp; rfl
_ ≤ n := by exact h2
simp at thish1 : n ≤ m can be handled by induction directly on the inductive definition of MyNat.le. The refl case is just \( n = n \), so rfl closes it immediately. In the step case, the goal becomes \( n \le m + 1 \), one step further than \( n \le m \), and I have both \( h : n \le m \) and \( h2 : m + 1 \le n \) available.
Chaining \( n \le m \), \( m < m + 1 \), and \( m + 1 \le n \) in a calc block gives \( n < n \). Since that contradicts the irreflexivity lemma proven above, simp spots the contradiction and closes the goal.
Having the mixed transitivity law and irreflexivity ready in advance meant the antisymmetry proof itself came down to a simple pattern: construct \( n < n \) and let that contradiction do the rest.
The full source code is available in the GitHub repository.
