In the previous articles, we showed that MyInt forms a partially ordered set. This time we continue by proving that MyInt is a total order, and further that it is an ordered ring. With both of these properties in place, powerful Mathlib automation tactics such as linarith and nlinarith become available, which makes proofs involving inequalities much easier to write. This article follows the corresponding chapter of ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発.
What is a total order
A binary relation on a set X is called a total order when it satisfies both of the following:
- X is a partially ordered set under the relation
- \( \forall x, y \in X,\ x \le y \lor y \le x \)
A partial order allows some elements to be incomparable, but in a total order any two elements are always comparable. Since MyInt is already known to be a partial order, all that remains is to show that any two elements are comparable.
Proving 0 ≤ a ∨ 0 ≤ -a
Rather than attacking \( a \le b \lor b \le a \) directly, we first prove the auxiliary lemma \( 0 \le a \lor 0 \le -a \). Since MyInt is defined as a quotient of the form \( m - n \), applying Quotient.inductionOn lets us pull out a representative pair (m, n), reducing the problem to an ordering statement about MyNat. We already have MyNat.le_total, so either n ≤ m or m ≤ n holds, and simp [mk_def] together with norm_cast translates that fact back into MyInt.
theorem MyInt.nonneg_or_nonneg_neg {a : MyInt} : 0 ≤ a ∨ 0 ≤ -a := by
induction a using Quotient.inductionOn with
| h a =>
obtain ⟨m, n⟩ := a
have : n ≤ m ∨ m ≤ n := by
exact MyNat.le_total n m
cases this with
| inl h =>
left
simp [mk_def]
norm_cast
| inr h =>
right
simp [mk_def]
norm_castProving MyInt.le_total
The main goal \( a \le b \lor b \le a \) can be rewritten as \( 0 \le b - a \lor 0 \le -(b - a) \), which lets us reuse the lemma above directly. Here the suffices tactic first establishes that proving this rewritten form is enough to close the original goal, and the actual proof of that form follows. Converting \( 0 \le b - a \) into \( a \le b \) uses the previously defined MyInt.sub_nonneg, and the other branch uses the abel tactic to automatically handle the commutative-group identity \( -(b-a) = a - b \).
theorem MyInt.le_total (a b : MyInt) : a ≤ b ∨ b ≤ a := by
suffices goal : 0 ≤ b - a ∨ 0 ≤ -(b -a) from by
cases goal with
| inl h =>
left
rw [← MyInt.sub_nonneg]
assumption
| inr h =>
right
rw [← MyInt.sub_nonneg]
rw [show -(b -a) = a - b from by abel] at h
assumption
exact MyInt.nonneg_or_nonneg_negRegistering the LinearOrder instance
With totality proven, we can register MyInt with Mathlib's LinearOrder type class. The le_total field is filled with the theorem above, and decidability (toDecidableLE) is derived automatically via infer_instance from the existing DecidableLE instance.
instance : LinearOrder MyInt where
le_total := MyInt.le_total
toDecidableLE := by infer_instanceThis registration unlocks the order tactic, which automatically searches for conclusions derivable from known facts about ≤, <, and = using only the axioms of a total order. For example, it can be used to close part of a case split, as shown below.
theorem MyInt.eq_or_lt_of_le {a b : MyInt} (h : a ≤ b) : a = b ∨ a < b := by
by_cases hor : a = b
case pos =>
left
assumption
case neg =>
right
order
theorem MyInt.le_of_eq_or_lt {a b : MyInt} (h : a = b ∨ a < b) : a ≤ b := by
cases h with
| inl h => rw [h]
| inr h => order
theorem MyInt.le_iff_eq_or_lt (m n : MyInt) : n ≤ m ↔ n = m ∨ n < m := by
constructor
case mp => apply MyInt.eq_or_lt_of_le
case mpr => apply MyInt.le_of_eq_or_ltWhat is an ordered ring
Next we show that MyInt is an ordered ring. An ordered ring is a set X with two binary operations forming a ring, together with the following two conditions:
- \( \forall x, y, z \in X,\ x \le y \to x + z \le y + z \)
- \( \forall x, y \in X,\ 0 \le x \land 0 \le y \to 0 \le x \cdot y \)
In other words, the order is always compatible with addition, and compatible with multiplication as long as both sides are nonnegative. Our goal is to register this as a Mathlib type class.
Rewriting strict order as an additive statement
MyInt's strict order \( a < b \) is defined as \( a \le b \land \lnot (b \le a) \). This raw logical form is awkward to work with in later proofs, so we first show it is equivalent to the statement "\( b \) is \( a \) plus some positive MyNat value", i.e. \( \exists k : \text{MyNat},\ a + (k + 1) = b \). Having this form available lets later proofs use induction and concrete computation on the MyNat side directly.
In lt.dest, notation_simp first unfolds the definition of \( a < b \), and we extract k from \( \exists k, a + k = b \) inside \( a \le b \). If k were 0 we would get \( a = b \), which contradicts the assumption \( \lnot (b \le a) \), so k must be nonzero and hence of the form \( k+1 \) for some k. The reverse direction, lt.intro, easily builds \( a \le b \) from the witness \( a + (k+1) = b \), but proving \( \lnot (b \le a) \) is more delicate: assuming \( b \le a \) leads to the contradiction \( 1 \le 0 \) via a calc block, closed at the end with the order tactic.
variable {a b c : MyInt}
theorem MyInt.lt.dest (h : a < b) : ∃ k : MyNat, a + (↑k + 1) = b := by
notation_simp at h
-- a b : MyInt
-- h : (∃ k, a + ↑k = b) ∧ ¬∃ k, b + ↑k = a
-- ⊢ ∃ k, a + (↑k + 1) = b
obtain ⟨⟨k, hk⟩, h⟩ := h
-- h : ¬∃ k, b + ↑k = a
-- k : MyNat
-- hk : a + ↑k = b
-- ⊢ ∃ k, a + (↑k + 1) = b
induction k with
| zero =>
exfalso
replace hk : a = b := by simp_all
have : ∃ k : MyNat, b + ↑k = a := by
rw [hk]
exists 0
simp
contradiction
| succ k _ =>
push_cast at hk
use k
assumption
theorem MyInt.le.intro (a : MyInt) (b : MyNat) : a ≤ a + ↑b := by
exact ⟨b, rfl⟩
theorem MyInt.lt.intro (h : ∃ k : MyNat, a + (k + 1) = b) : a < b := by
obtain ⟨k, hk⟩ := h
simp only [lt_def] -- ⊢ a ≤ b ∧ ¬b ≤ a
constructor
case left => -- ⊢ a ≤ b
notation_simp
use k + 1
assumption
case right => -- ⊢ ¬b ≤ a
notation_simp
intro ⟨s, hs⟩
rw [← hs] at hk
-- hk : a + (↑k + 1) = b
-- hs : b + ↑s = a
-- ⊢ a + (↑k + 1) = b
have : ↑(s + k) + (1 : MyInt) = 0 := calc
_ = (↑s + ↑k) + (1 : MyInt) := by push_cast; ac_rfl
_ = (b + ↑s + (↑k + 1)) - b := by abel
_ = b - b := by rw [hk]
_ = 0 := by abel
replace : (0 : MyInt) > 0 := calc
_ = ↑(s + k) + (1 : MyInt) := by rw [this]
_ = (1 : MyInt) + ↑(s + k):= by ac_rfl
_ ≥ (1 : MyInt) := by apply MyInt.le.intro
_ > (0 : MyInt) := by decide
order
theorem MyInt.lt_iff_add : a < b ↔ ∃ k : MyNat, a + (k + 1) = b := by
constructor
case mp => exact MyInt.lt.dest
case mpr => exact MyInt.lt.introProving multiplication preserves strict order
Next we show \( a < b \land 0 < c \to c \cdot a < c \cdot b \). As preparation, we register ofMyNat_mul, which shows that MyNat multiplication commutes with the cast into MyInt, tagged with the @[push_cast] attribute so that the push_cast tactic will apply it automatically in later proofs.
In mul_pos, both \( 0 < a \) and \( 0 < b \) are unfolded into the \( \exists k, \dots \) form from above, rewriting \( a \) as \( 0 + (c+1) \) and \( b \) as \( 0 + (d+1) \), and \( c \cdot d + c + d \) is offered as the witness for the product. push_cast and ring then mechanically confirm the resulting equality. sub_pos is a lemma connecting subtraction and ordering, \( 0 < a - b \leftrightarrow b < a \), which lets the proof of \( c \cdot a < c \cdot b \) be reduced to "just show \( 0 < c \cdot (b-a) \)", a form where mul_pos applies directly.
@[push_cast]
theorem MyInt.ofMyNat_mul (m n : MyNat) : ↑(m * n) = (m : MyInt) * (n : MyInt) := by
dsimp [MyInt.ofMyNat]
apply Quotient.sound
notation_simp
ring
theorem MyInt.mul_pos (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
rw [MyInt.lt_iff_add] at *
obtain ⟨c, hc⟩ := ha
obtain ⟨d, hd⟩ := hb
-- hc : 0 + (↑c + 1) = a
-- hd : 0 + (↑d + 1) = b
-- ⊢ ∃ k, 0 + (↑k + 1) = a * b
rw [← hc, ← hd] -- ⊢ ∃ k, 0 + (↑k + 1) = (0 + (↑c + 1)) * (0 + (↑d + 1))
use c * d + c + d
push_cast
ring
theorem MyInt.sub_pos : 0 < a - b ↔ b < a := by
constructor <;> intro h
· rw [MyInt.lt_iff_add] at *
obtain ⟨k, hk⟩ := h
simp at hk
use k
rw [hk]
abel
· rw [MyInt.lt_iff_add] at *
obtain ⟨k, hk⟩ := h
use k
rw [← hk]
abel
theorem MyInt.mul_lt_mul_of_pos_left (h : a < b) (pos : 0 < c)
: c * a < c * b := by
suffices 0 < c * (b - a) from by
-- h : a < b
-- pos : 0 < c
-- this : 0 < c * (b - a)
-- ⊢ c * a < c * b
rw [MyInt.lt_iff_add] at this ⊢
-- this : ∃ k, 0 + (↑k + 1) = c * (b - a) ⊢ ∃ k, c * a + (↑k + 1) = c * b
obtain ⟨k, hk⟩ := this
simp at hk
use k
rw [hk]
simp [MyInt.left_distrib]
replace h : 0 < b - a := by
rw [MyInt.sub_pos]
assumption
apply MyInt.mul_pos (ha := pos) (hb := h)
theorem MyInt.mul_lt_mul_of_pos_right (h : a < b) (pos : 0 < c)
: a * c < b * c := by
rw [MyInt.mul_comm a c, MyInt.mul_comm b c]
apply MyInt.mul_lt_mul_of_pos_left (h := h) (pos := pos)
instance : IsStrictOrderedRing MyInt where
zero_le_one := by decide
exists_pair_ne := by exists 0, 1
mul_lt_mul_of_pos_left := by
intro a ha b c hbc
exact MyInt.mul_lt_mul_of_pos_left hbc ha
mul_lt_mul_of_pos_right := by
intro c hc a b hab
exact MyInt.mul_lt_mul_of_pos_right hab hcFinally, we bundle these into the IsStrictOrderedRing type class, which expresses compatibility between the ring operations and the strict order. It also requires zero_le_one (ordering of 0 and 1) and exists_pair_ne (existence of two distinct elements, i.e. that the ring is nontrivial).
Using the linarith tactic
Registering MyInt as an ordered ring unlocks the linarith tactic. When every hypothesis and the goal can be expressed as linear equalities or inequalities, linarith automatically combines them to derive a contradiction or the goal, saving the trouble of manual algebraic manipulation.
example (h : a < b) : a + c < b + c := by
linarith
example (h1 : 2 * a - b = 1) (h2 : a + b = 5) : a = 2 := by
linarithIn practice, however, numeric literals such as 2 or 5 did not work smoothly at first. The cause was that the successor rule for the natural-number cast (natCast_succ) was not correctly set up in MyInt's CommRing instance. We fixed this by proving ofNat_succ, which shows that MyInt.ofNat is compatible with the successor operation, and wiring it explicitly into the CommRing instance.
theorem MyInt.ofNat_succ (n : Nat) : MyInt.ofNat (n + 1) = MyInt.ofNat n + 1 := by
apply Quotient.sound
notation_simp
simp [MyInt.ofNat, MyNat.ofNat]
change (MyNat.ofNat n).succ = MyNat.ofNat n + MyNat.succ 0
exact (MyNat.add_succ (MyNat.ofNat n) 0).symm
instance : CommRing MyInt where
natCast := MyInt.ofNat
natCast_zero := rfl
natCast_succ := MyInt.ofNat_succNon-strict order under multiplication, and nlinarith
Finally we show the non-strict version, \( 0 \le c \land a \le b \to c \cdot a \le c \cdot b \). This follows logically from the strict-order results and the other ring and order axioms proven so far, but rather than assembling the proof by hand, we hand it off to the nlinarith tactic. nlinarith extends linarith by also trying simple nonlinear combinations, such as products of hypotheses, before searching for a linear contradiction, which makes it directly applicable to statements like this one that involve multiplication.
theorem MyInt.mul_le_mul_of_nonneg_left (h : a ≤ b) (nneg: 0 ≤ c)
: c * a ≤ c * b := by
nlinarith
theorem MyInt.mul_le_mul_of_nonneg_right (h : a ≤ b) (nneg: 0 ≤ c)
: a * c ≤ b * c := by
nlinarith
instance : IsOrderedRing MyInt where
zero_le_one := by decide
mul_le_mul_of_nonneg_left := by
intro a ha b c hbc
exact MyInt.mul_le_mul_of_nonneg_left hbc ha
mul_le_mul_of_nonneg_right := by
intro c hc a b hab
exact MyInt.mul_le_mul_of_nonneg_right hab hc
example (h1 : 3 * a - 2 * b = 5) (h2: 6 * a - 5 * b = 11)
: b = -1 := by nlinarithWith this, the IsOrderedRing registration is complete, and nonlinear equalities and inequalities can now be proven with nlinarith alone.
Summary
In this article we proved that MyInt is a total order and an ordered ring, registering it with the LinearOrder, IsStrictOrderedRing, and IsOrderedRing type classes. As a result, the powerful automation tactics order, linarith, and nlinarith are now all available for MyInt. This series does not cover the textbook's grind tactic, but with this article, all of the textbook's content has been covered.
The full code is available at https://github.com/ringring-creator/LearnLean.
