norm_num introduces Classical.choice on order goals over Nat/Int where decide does not

norm_num closes numeric order goals over ℕ and ℤ with a proof depending on Classical.choice. decide and simp close the same goals without it. Equality and disequality goals are unaffected.

import Mathlib

theorem a : (2 : ℤ) ≤ 4 := by norm_num
theorem b : (2 : ℤ) ≤ 4 := by decide
theorem c : (2 : ℤ) ≤ 4 := by simp
theorem d : (2 : ℤ) + 2 = 4 := by norm_num

#print axioms a -- propext, Classical.choice, Quot.sound
#print axioms b -- propext
#print axioms c -- propext
#print axioms d -- propext

Same for <, ≥, > and over ℕ.

The route:

a -> Mathlib.Meta.NormNum.isNat_le_true -> Nat.mono_cast -> monotone_nat_of_le_succ -> Nat.rel_of_forall_rel_succ_of_le -> LE.le.eq_or_lt -> eq_or_lt_of_le -> lt_or_eq_of_le -> Classical.propDecidable -> Classical.choice

lt_or_eq_of_le is stated for a general PartialOrder, where equality is not decidable, so its use of Classical.propDecidable is correct. The issue is that the norm_num order extension only ever runs on types that do have DecidableEq, and inherits the general lemma's classical dependence anyway.

A constructive route exists on ℤ:

theorem e (a b : ℤ) (h : a ≤ b) : a < b ∨ a = b := by
by_cases hab : a = b
· exact Or.inr hab
· exact Or.inl (Int.lt_iff_le_and_ne.mpr ⟨h, hab⟩)

#print axioms e -- propext

Lean 4.32.1.

Start at Mathlib.Meta.NormNum.isNat_le_true and trace the order-proof route through Nat.mono_cast, monotone_nat_of_le_succ, and the related order lemmas. Run the supplied Lean examples with #print axioms; done means numeric order goals over Nat and Int no longer depend on Classical.choice while equality and disequality behavior remains unchanged.