Aligning `Nat.le`

[dselsam]

Lean4's ≤ does not match lean3's ≤ on nats. In lean3, nat.le are inductive whereas in lean4, Nat.le is defined as the boolean version returning true. I think this instance clash will cause big problems and needs to be fixed.

According to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/226097604 this seems like it could be a manageable (if unpleasant) backport to mathlib, since only a few places seem to inspect the internals of ≤. However, it may be acceptable to just change the Lean4 version, i.e. with something like:

axiom Nat.le2 : Nat → Nat → Prop
axiom Nat.leOfTrue  {m n : Nat} : Nat.ble m n = true     → Nat.le2 m n
axiom Nat.leOfFalse {m n : Nat} : ¬ (Nat.ble m n = true) → ¬ Nat.le2 m n

instance (m n : Nat) : Decidable (Nat.le2 m n) :=
  if h : Nat.ble m n = true then isTrue (Nat.leOfTrue h)
  else isFalse (Nat.leOfFalse h)

Leo's call.

[digama0]

Here's a proof that an inductive type alignable with nat.less_than_or_equal coheres with Nat.ble, for your convenience:

namespace Nat

inductive le' (a : Nat) : Nat → Prop
  | refl : le' a a
  | step {b} : le' a b → le' a (succ b)

theorem zero_le' : (n : Nat) → le' 0 n
  | zero => le'.refl
  | succ n => le'.step (zero_le' n)

theorem succ_le'_succ : {m n : Nat} → le' m n → le' (succ m) (succ n)
  | _, _, le'.refl => le'.refl
  | _, _, le'.step h => le'.step (succ_le'_succ h)

theorem le_of_true : {m n : Nat} → ble m n = true → le' m n
  | zero, n, _ => zero_le' n
  | succ m, succ n, h => succ_le'_succ (le_of_true h)

theorem ble_self : (n : Nat) → ble n n = true
  | zero => rfl
  | succ n => ble_self n

theorem ble_succ : {m n : Nat} → ble m n = true → ble m (succ n) = true
  | zero, _, _ => rfl
  | succ m, succ n, h => @ble_succ m n h

theorem true_of_le : {m n : Nat} → le' m n → ble m n = true
  | n, _, le'.refl => ble_self n
  | m, _, @le'.step m n h => ble_succ (true_of_le h)

instance (m n : Nat) : Decidable (Nat.le' m n) :=
  if h : ble m n = true then isTrue (Nat.le_of_true h)
  else isFalse (mt true_of_le h)

end Nat