This time we prove that MyInt is a commutative ordered group under addition. Once this is established, we can freely use Mathlib's lemmas and tactics about order on MyInt as well. We also register decidable instances so the comparison operator \( \le \) becomes computable. This article follows along with the book ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発.
What is an ordered group
An ordered group is a group equipped with an order such that the group operation preserves that order. Concretely, it satisfies the following two properties.
\( \forall x, y, z \in X,\ x \le y \to x + z \le y + z \)
\( \forall x, y, z \in X,\ x \le y \to z + x \le z + y \)
Proving MyInt is an ordered group
First we prove add_le_add_left, which corresponds to the first property.
theorem MyInt.add_le_add_left (a b : MyInt) (h : a ≤ b) (c : MyInt)
: a + c ≤ b + c := by
notation_simp at *
obtain ⟨m, hm⟩ := h
use m
-- hm : a + ↑m = b
-- ⊢ a + c + ↑m = b + c
have : a + c + ↑m = b + c := calc
_ = c + (a + ↑m) := by ac_rfl
_ = c + b := by rw [hm]
_ = b + c := by ac_rfl
assumptionUnfolding the definition of a ≤ b reduces the goal to finding a natural number m such that b = a + m. From there, ac_rfl rearranges the terms using commutativity and associativity of addition to close the proof.
To make this property available to Mathlib, we register it as an instance of IsOrderedAddMonoid.
instance : IsOrderedAddMonoid MyInt where
add_le_add_left := MyInt.add_le_add_leftMaking the comparison operator computable
We now know MyInt is an ordered group, but as it stands ≤ only exists as a proposition; we cannot actually compute whether it holds. To use the decide tactic or #eval, we need to register a Decidable instance.
The approach is the same as with MyNat: reduce decidability of n ≤ m to decidability of 0 ≤ m - n. As a stepping stone, we first show that 0 ≤ n is decidable.
We start by defining a function bpos that computes 0 ≤ n.
-- n1 - n2 ≥ 0
def PreInt.bpos (n : PreInt) : Bool :=
match n with
| (n1, n2) => decide (n2 ≤ n1)
-- n1 - n2 ≥ 0 for MyInt
def MyInt.bpos : MyInt → Bool := Quotient.lift PreInt.bpos <| by
intro (a1, a2) (b1, b2) hr
notation_simp at hr
-- hr : a1 + b2 = a2 + b1
-- ⊢ PreInt.bpos (a1, a2) = PreInt.bpos (b1, b2)
dsimp [PreInt.bpos]
-- ⊢ PreInt.bpos (a1, a2) = PreInt.bpos (b1, b2)
suffices a2 ≤ a1 ↔ b2 ≤ b1 from by
simp_all
constructor <;> intro h
case mp =>
have : a1 + b2 ≤ a1 + b1 := calc
_ = a2 + b1 := by rw [hr]
_ ≤ a1 + b1 := by compatible
simp at this
assumption
case mpr =>
have : a2 + b1 ≤ a1 + b1 := calc
_ = a1 + b2 := by rw [hr]
_ ≤ a1 + b1 := by compatible
simp at this
assumption
@[simp]
theorem MyInt.bpos_def (m n : MyNat) : MyInt.bpos (⟦(m, n)⟧) = true ↔ n ≤ m := by
dsimp [MyInt.bpos, PreInt.bpos]
simpSince MyInt.bpos is a function on the quotient type MyInt, it is defined using Quotient.lift together with a proof that it is well-defined. That proof shows the result does not depend on the choice of representative, using the equivalence relation hr.
Next, we prepare the lemmas needed to prove MyInt.bpos z = true ↔ 0 ≤ z.
@[norm_cast]
theorem MyInt.ofMyNat_le (m n : MyNat) : (m : MyInt) ≤ (n : MyInt) ↔ m ≤ n := by
rw [MyNat.le_iff_add]
notation_simp
constructor <;> intro ⟨k, hk⟩
case mp =>
use k
have : ↑(m + k) = (n : MyInt) := by
norm_cast at hk
norm_cast at *
case mpr =>
use k
rw [← hk]
norm_cast
theorem MyInt.le_sub_iff (x y z : MyInt) : z ≤ x - y ↔ z + y ≤ x := by
notation_simp
constructor <;> intro ⟨k, hk⟩
case mp =>
use k
have : z + y + ↑k = x := calc
_ = z + ↑k + y := by ac_rfl
_ = (x - y) + y := by simp [hk]
_ = x := by abel
assumption
case mpr =>
use k
have : z + ↑k = x - y:= calc
_ = (z + y + ↑k) - y := by abel
_ = x - y := by rw [hk]
assumption
theorem MyInt.sub_nonneg (m n : MyInt) : 0 ≤ m - n ↔ n ≤ m := by
have := MyInt.le_sub_iff m n 0
simp_allofMyNat_le shows that the order on MyNat is preserved by the embedding into MyInt, while le_sub_iff and sub_nonneg rewrite inequalities into a subtraction form. Combining these gives us the theorem we're after.
theorem MyInt.bpos_iff (z : MyInt) : MyInt.bpos z = true ↔ 0 ≤ z := by
induction z using Quotient.inductionOn with
| h a =>
obtain ⟨x, y⟩ := a
rw [MyInt.bpos_def, MyInt.mk_def]
rw [MyInt.sub_nonneg]
norm_castinduction z using Quotient.inductionOn with replaces the statement about an element \( z \in \text{MyInt} \) of the quotient type with a statement about a representative \( a \in \text{MyNat} \times \text{MyNat} \) of its equivalence class. From there, applying the lemmas we prepared closes the proof.
We now register this decidability with DecidablePred so the decide tactic can be used.
instance : DecidablePred (0 ≤ · : MyInt → Prop) := by
intro n
apply decidable_of_iff (MyInt.bpos n = true)
exact MyInt.bpos_iff n
example : 0 ≤ (3 : MyInt) := by
decideWe also register decidability of n ≤ m as an instance of DecidableLE.
instance : DecidableLE MyInt := by
intro n m
apply decidable_of_iff (0 ≤ m - n)
exact MyInt.sub_nonneg m nWe can now confirm this is evaluable with #eval and that the decide tactic works.
#eval (3 : MyInt) ≤ 4
example : (3 : MyInt) ≤ 4 := by
decideWe do the same for the strict order. infer_instance is an instruction meaning "solve this goal with an instance the system already knows about." After dsimp rewrites the goal into the form n m : MyInt ⊢ Decidable (n ≤ m ∧ ¬m ≤ n), it can be solved by the Decidable instance for the non-strict order that we already registered.
instance : DecidableLT MyInt := by
intro n m
dsimp [(· < ·), MyInt.lt]
infer_instance
#eval (3 : MyInt) < 4
example : (3 : MyInt) < 4 := by
decideFinally, we register an instance for equality as well. Using the relation x = y ↔ x ≤ y ∧ y ≤ x, it can be computed from the existing DecidableLE instance.
instance : DecidableEq MyInt := decidableEqOfDecidableLE
#eval (3 : MyInt) = 4
example : ¬ (3 : MyInt) = 4 := by
decideMyInt can now be treated as an ordered group, and all of its comparison operators are computable. The code is available in the repository below.
