ホーム / Technical /

Making MyNat's Order Relation Decidable — Proving with ble and inductAux

Friday, 14 August 2026

Lean Mathematics Technical

t f B! P L

This post is part of my notes on learning Lean using "ゼロから始めるLean言語入門" (roughly, "Learning Lean from Scratch") as the textbook.

This time I look at proving concrete numeric order relations. Repeatedly applying MyNat.le.step lets you prove individual propositions, but writing a separate proof for every statement isn't very efficient. So I prepare a more general way to decide order relations.

The brute-force proof looks like this.

example : 0 ≤ 3 := by
  apply MyNat.le.step
  apply MyNat.le.step
  apply MyNat.le.step
  apply MyNat.le.refl

The Decidable Type Class

This is where the Decidable type class comes in. Decidable expresses that a proposition is decidable, meaning its truth value can be determined by computation, and it provides the mechanism for using that computed result in a proof.

Introducing DecidableEq

Since wanting equality to be a Decidable instance is common, Lean provides a dedicated DecidableEq type class. Using the deriving keyword, an instance can be derived automatically for an existing type.

The declaration below registers MyNat as a DecidableEq using deriving. Once registered, equalities and inequalities can be proved with the decide tactic, and the computed result can also be checked directly with #eval.

deriving instance DecidableEq for MyNat

example : 32 + 13 ≠ 46 := by
  decide

#eval 32 + 13 ≠ 46

Defining MyNat.ble

Next, as preparation for registering the order relation as Decidable, I define a function that returns a boolean. MyNat.ble a b returns true whenever \(a \le b\) holds.

-- bool less than or equals to
def MyNat.ble (a b : MyNat) : Bool :=
  match a, b with
  | 0, _ => true
  | _ + 1, 0 => false
  | a + 1, b + 1 => MyNat.ble a b

#eval MyNat.ble 0 0 -- true
#eval MyNat.ble 3 4 -- true
#eval MyNat.ble 4 3 -- false

Registering DecidableLE

To register DecidableLE, the Decidable class for the order relation, I need to prove MyNat.ble m n = true ↔ m ≤ n.

instance : DecidableLE MyNat := fun n m =>
  decidable_of_iff (MyNat.ble n m = true) (MyNat.le_impl n m)

Proving the Auxiliary Lemmas

Before tackling the main proof, I prove a few lemmas I'll need. Each follows directly from the definition, so rfl is enough.

@[simp]
theorem MyNat.ble_zero_left (n : MyNat) : MyNat.ble 0 n = true := by
  rfl

@[simp]
theorem MyNat.ble_zero_right (n : MyNat) : MyNat.ble (n + 1) 0 = false := by
  rfl

@[simp]
theorem MyNat.ble_succ (m n : MyNat) : MyNat.ble (m + 1) (n + 1) = MyNat.ble m n := by rfl

Proving MyNat.le_impl

Because MyNat.ble is defined inductively with case splits, the ordinary induction tactic can't split cases the way the definition does. So I use the auxiliary function MyNat.ble.inductAux and pass it to induction ... using, which performs induction following the same case split as ble's definition.

theorem MyNat.le_impl (m n : MyNat) : MyNat.ble m n = true ↔ m ≤ n := by
  induction m, n using MyNat.ble.inductAux with
  | case1 n => simp
  | case2 n =>
    suffices ¬ n + 1 ≤ 0 from by simp_all
    intro h
    simp_all
  | case3 m n ih =>
    simp [ih]

case1 corresponds to MyNat.ble 0 n = true ↔ 0 ≤ n. Since MyNat.ble_zero_left makes the left side always true, simp alone proves it.

case2 corresponds to MyNat.ble (n + 1) 0 = true ↔ n + 1 ≤ 0. Since MyNat.ble_zero_right makes the left side always false, it suffices to show ¬ n + 1 ≤ 0. This is done by deriving a contradiction from the assumption n + 1 ≤ 0 with simp_all.

case3 corresponds to MyNat.ble (m + 1) (n + 1) = true ↔ m + 1 ≤ n + 1, and it's proved with simp using the induction hypothesis ih, MyNat.ble m n = true ↔ m ≤ n.

Note that the textbook uses dsimp [MyNat.ble] in case2 and case3, but when I actually tried it, it resulted in a "no progress" error, so I've left it out here.

Now numeric order relations can be evaluated by computation.

#eval 0 ≤ 0 -- true
#eval 1 ≤ 3 -- true
#eval 3 ≤ 1 -- false

Extending to Strict Order

I follow the same steps for strict order as I did for the (non-strict) order relation.

theorem MyNat.lt_impl (m n : MyNat) : MyNat.ble (m + 1) n ↔ m < n := by
  rw [MyNat.le_impl]
  rfl

instance : DecidableLT MyNat := fun n m =>
  decidable_of_iff (MyNat.ble (n + 1) m = true) (MyNat.lt_impl n m)

example : 1 < 4 := by
  decide

The code is available in the following repository.

https://github.com/ringring-creator/LearnLean

QooQ