ホーム / Technical /

Registering MyInt as a Preorder

Saturday, 15 August 2026

Lean Mathematics Technical

t f B! P L

This time, we'll make MyInt usable as an ordered set. We'll start by introducing preorders, set up a cast from MyNat to MyInt, define the non-strict and strict orders, and finally register MyInt as an instance of Mathlib's Preorder type class so that the order tactic becomes available. This article follows along with "ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発".

What is a preorder?

A binary relation on a set X is called a preorder when it satisfies the following two properties.

Reflexivity: \( \forall x \in X,\ x \le x \)
Transitivity: \( \forall x, y, z \in X,\ x \le y \land y \le z \to x \le z \)

MyInt satisfies both of these properties, so it can be treated as a preorder. We'll register it as an instance of Mathlib's Preorder type class.

Treating MyNat as MyInt

Before defining the order, we need a way to treat natural numbers as integers. Currently, passing a MyNat directly to a function expecting MyInt results in an error. 

private def MyInt.const (z : MyInt) : MyInt → MyInt := fun _ => z

#check_failure MyInt.const (0 : MyNat)

It needs to be converted before being passed in as MyInt, like this. 

def MyInt.ofMyNat (n : MyNat) : MyInt := ⟦(n, 0)⟧

#check MyInt.const (.ofMyNat 0)

Using Lean 4's type coercion mechanism, we can force MyNat to convert into MyInt. 

instance : Coe MyNat MyInt where
  coe := MyInt.ofMyNat

-- (MyInt.ofMyNat 0).const : MyInt → MyInt
#check MyInt.const (0 : MyNat)

However, with this approach the conversion always happens forcibly, rather than acting as a genuine cast. 

example : ((0 : MyNat): MyInt) = (0 : MyInt) := by
  guard_target =ₛ MyInt.ofMyNat 0 = 0
  sorry

Types that are in a subset relationship, like MyNat and MyInt, are more convenient to treat as casts. This can be achieved by registering MyInt.ofMyNat with the coe attribute. 

attribute [coe] MyInt.ofMyNat

Looking at the example again, we can see that MyNat is now treated as a cast, written ↑(0 : MyNat). The ↑ symbol indicates a type cast. 

@[simp]
theorem MyInt.ofMyNat_zero_eq_zero : MyInt.ofMyNat 0 = (0: MyInt) := by
  dsimp [MyInt.ofMyNat]
  rfl

example : ((0 : MyNat): MyInt) = (0 : MyInt) := by
  guard_target =ₛ ↑(0 : MyNat) = (0 : MyInt)
  simp

Proving the cast is injective

Next we prove that this cast is injective. The norm_cast attribute registers a lemma with the tactics that handle type casts. 

@[norm_cast]
theorem MyInt.ofMyNat_inj {m n : MyNat}
  : (m : MyInt) = (n : MyInt) ↔ m = n := by
    constructor <;> intro h
    case mp =>
      have : (m, 0) ≈ (n, 0) := by
        exact Quotient.exact h
      notation_simp at this
      simp_all
    case mpr =>
      rw [h]

The norm_cast tactic can then be used as follows. 

@[simp]
theorem MyInt.ofMyNat_eq_zero {n : MyNat} : (n : MyInt) = 0 ↔ n = 0 := by
  constructor <;> intro h
  · rw [show (0 : MyInt) = ↑ (0 : MyNat) from rfl] at h
    norm_cast at h
  · simp_all

Registering the push_cast attribute makes casts get pushed inward before tactics like ring run, expanding the cast into the inside of the parentheses. 

@[push_cast]
theorem MyInt.ofNat_add (m n : MyNat)
  : ↑ (m + n) = (m : MyInt) + (n : MyInt) := by
    rfl

Defining non-strict and strict order on MyInt

We define the non-strict order (≤) and strict order (<) on MyInt. 

def MyInt.le (m n : MyInt) : Prop :=
  ∃ k : MyNat, m + ↑ k = n

instance : LE MyInt where
  le := MyInt.le

@[notation_simp]
theorem MyInt.le_def (m n : MyInt) : m ≤ n ↔ ∃ k : MyNat, m + ↑ k = n := by
  rfl

def MyInt.lt (m n : MyInt) : Prop :=
  m ≤ n ∧ ¬ n ≤ m

instance : LT MyInt where
  lt := MyInt.lt

@[notation_simp]
theorem MyInt.lt_def (a b : MyInt) : a < b ↔ a ≤ b ∧ ¬ (b ≤ a) := by
  rfl

Proving reflexivity

@[refl]
theorem MyInt.le_refl (m : MyInt) : m ≤ m := by
  exists 0
  simp

Proving transitivity

Next we prove transitivity. The key steps are rewriting into sum form with notation_simp, turning the goal into ⊢ n + ↑(a + b) = k with use a + b, and then into ⊢ n + (↑a + ↑b) = k with push_cast. From there, the hypotheses and ac_rfl get us to the goal. 

theorem MyInt.le_trans {m n k : MyInt} (hnm: n ≤ m) (hmk: m ≤ k) : n ≤ k := by
  notation_simp at *
  obtain ⟨a, ha⟩ := hnm
  obtain ⟨b, hb⟩ := hmk
  -- a : MyNat
  -- ha : n + ↑a = m
  -- b : MyNat
  -- hb : m + ↑b = k
  -- ⊢ ∃ k_1, n + ↑k_1 = k
  use a + b -- ⊢ n + ↑(a + b) = k
  push_cast -- ⊢ n + (↑a + ↑b) = k

  have : n + (↑ a + ↑ b) = k := calc
    _ = (n + ↑ a) + ↑ b := by ac_rfl
    _ = m + ↑ b := by rw [ha]
    _ = k := by rw [hb]
  assumption

We register transitivity with the Trans class so it can be used with the calc tactic. 

instance : Trans (· ≤ · : MyInt → MyInt → Prop) (· ≤ ·) (· ≤ ·) where
  trans := MyInt.le_trans

Registering as a Preorder

Finally, we register MyInt as a preorder so that the order tactic becomes available. 

instance : Preorder MyInt where
  le_refl := MyInt.le_refl
  le_trans := by
    intro a b c hab hbc
    apply MyInt.le_trans hab hbc

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

With the Preorder instance registered, the order tactic can now handle reflexivity and transitivity automatically.

The code is available in the GitHub repository.

QooQ