Proving Antisymmetry and Registering MyInt as a PartialOrder in Lean 4

In this article, we prove that MyInt satisfies the properties of a partial order. As always, the reference book is ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発.

What Is a Partial Order

A binary relation on a set X is called a partial order when it satisfies:

• X is a preorder with respect to the relation
• Antisymmetry holds: \( \forall x, y \in X,\ x \le y \land y \le x \to x = y \)

We already proved reflexivity and transitivity (the preorder part) in earlier articles, so this time we focus on proving antisymmetry.

A Lemma for the Antisymmetry Proof

First, we prepare a lemma: if a + b = a then b = 0.

@[simp ↓]
theorem MyInt.add_right_eq_self {a b : MyInt} : a + b = a ↔ b = 0 := by
  constructor <;> intro h
  case mp => calc
    -- h : a + b = a ⊢ b = 0
    _ = b := by rfl
    _ = a + b - a := by abel
    _ = a - a := by rw [h]
    _ = 0 := by abel
  case mpr => simp [h]

For the mp direction, the calc block rewrites b as a + b - a, substitutes a with a + b using the hypothesis h, and simplifies with abel to reach 0. The mpr direction is a straightforward substitution, so a single simp call suffices. The @[simp ↓] attribute registers the lemma so it gets applied automatically by simp from now on.

Proving Antisymmetry

Now for the main proof: deriving a = b from a ≤ b and b ≤ a. Since ≤ is defined in terms of a natural number difference, we unfold it with notation_simp and extract the witnesses with obtain.

theorem MyInt.le_antisymm (a b : MyInt) (h1: a ≤ b) (h2: b ≤ a) : a = b := by
  notation_simp at *
  obtain ⟨m, hm⟩ := h1
  obtain ⟨n, hn⟩ := h2
  -- hm : a + ↑m = b
  -- hn : b + ↑n = a
  -- ⊢ a = b
  have : a + (↑m + ↑n) = a := calc
    _ = a + ↑m + ↑n := by ac_rfl
    _ = b + ↑n := by rw [hm]
    _ = a := by rw[hn]

  replace : ↑(m + n) = (0 : MyInt) := by
    push_cast
    simp_all

  have : m = 0 ∧ n = 0 := by
    simp_all
  simp_all

The idea is to combine hm and hn into the equation a + (↑m + ↑n) = a. The calc block rewrites using associativity and commutativity via ac_rfl, then substitutes with hm and hn in turn.

Applying the earlier lemma to this equation gives ↑m + ↑n = 0, i.e. ↑(m + n) = 0. replace works just like have, except it overwrites the existing this. Here it takes the this produced by the previous have and, via push_cast and simp_all, converts it into an equation over MyNat.

Since a sum of natural numbers is zero only when both are zero, we get m = 0 ∧ n = 0. Substituting back into hm with simp_all then yields a = b, completing the proof.

Registering with PartialOrder

Finally, we register the instance with PartialOrder. The preorder portion is already registered, so only le_antisymm needs to be added.

instance : PartialOrder MyInt where
  le_antisymm := by apply MyInt.le_antisymm

example (a b : MyInt) (h1: a ≤ b) (h2: b ≤ a) : a = b := by
  order

Once registered, the order tactic becomes available. It automatically uses the structure of preorders, partial orders, linear orders, and so on to close order-related goals, which will significantly simplify future proofs.

The full code is available in the GitHub repository.