feat: Nat.{div,mod} to use fuel, not fix (#7558)

This PR changes the definition of `Nat.div` and `Nat.mod` to use a
structurally recursive, fuel-based implementation rather than
well-founded recursion. This leads to more predicable reduction behavior
in the kernel.

`Nat.div` and `Nat.mod` are somewhat special because the kernel has
native reduction for them when applied to literals. But sometimes this
does not kick in, and the kernel has to unfold `Nat.div`/`Nat.mod` (e.g.
in `lazy_delta_reduction` when there are open terms around). In these
cases we want a well-behaved definition.

We really do not want to reduce proofs in the kernel, which we want to
prevent anyways well-founded recursion (to be prevented by #5182).

Hence we avoid well-founded recursion here, and use a (somewhat
standard) translation to a fuel-based definition.

(If this idiom is needed more often we could even support it in Lean
with `termination_by +fuel <measure>` rather easily.)

src/Init/Data/Nat/Div/Basic.lean

@@ -20,20 +20,56 @@ instance : Dvd Nat where
 theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
   fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
 
+theorem div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) :
+    x - y < fuel :=
+  Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel)
+
 @[extern "lean_nat_div"]
 protected def div (x y : @& Nat) : Nat :=
-  if 0 < y ∧ y ≤ x then
-    Nat.div (x - y) y + 1
+  if hy : 0 < y then
+    let rec
+      go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
+      match fuel with
+      | 0 => by contradiction
+      | succ fuel =>
+        if h : y ≤ x then
+          go fuel (x - y) (div_rec_fuel_lemma hy h hfuel) + 1
+        else
+          0
+      termination_by structural fuel
+    go (x + 1) x (Nat.lt_succ_self _)
   else
     0
-decreasing_by apply div_rec_lemma; assumption
 
 instance instDiv : Div Nat := ⟨Nat.div⟩
 
+private theorem div.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
+    Nat.div.go y hy fuel1 x h1 = Nat.div.go y hy fuel2 x h2 := by
+  match fuel1, fuel2 with
+  | 0, _ => contradiction
+  | _, 0 => contradiction
+  | succ fuel1, succ fuel2  =>
+    simp only [Nat.div.go]
+    split
+    next => rw [Nat.div.go.fuel_congr]
+    next => rfl
+termination_by structural fuel1
+
 theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
-  show Nat.div x y = _
-  rw [Nat.div]
-  rfl
+  show Nat.div _ _ = ite _ (Nat.div _ _ + 1) _
+  unfold Nat.div
+  split
+  next =>
+    rw [Nat.div.go]
+    split
+    next =>
+      simp only [and_self, ↓reduceIte, *]
+      congr 1
+      apply div.go.fuel_congr
+    next =>
+      simp only [and_false, ↓reduceIte, *]
+  next =>
+    simp only [false_and, ↓reduceIte, *]
 
 def div.inductionOn.{u}
       {motive : Nat → Nat → Sort u}
@@ -72,22 +108,61 @@ theorem div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n := by
     have := Nat.add_le_of_le_sub hKN this
     exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this
 
-@[extern "lean_nat_mod"]
-protected def modCore (x y : @& Nat) : Nat :=
+protected noncomputable def modCore (x y : Nat) : Nat :=
+  if hy : 0 < y then
+    let rec
+      go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
+      match fuel with
+      | 0 => by contradiction
+      | succ fuel =>
+        if h : y ≤ x then
+          go fuel (x - y) (div_rec_fuel_lemma hy h hfuel)
+        else
+          x
+      termination_by structural fuel
+    go (x + 1) x (Nat.lt_succ_self _)
+  else
+    x
+
+private theorem modCore.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
+    Nat.modCore.go y hy fuel1 x h1 = Nat.modCore.go y hy fuel2 x h2 := by
+  match fuel1, fuel2 with
+  | 0, _ => contradiction
+  | _, 0 => contradiction
+  | succ fuel1, succ fuel2  =>
+    simp only [Nat.modCore.go]
+    split
+    next => rw [Nat.modCore.go.fuel_congr]
+    next => rfl
+termination_by structural fuel1
+
+protected theorem modCore_eq (x y : Nat) : Nat.modCore x y =
   if 0 < y ∧ y ≤ x then
     Nat.modCore (x - y) y
   else
-    x
-decreasing_by apply div_rec_lemma; assumption
+    x := by
+  unfold Nat.modCore
+  split
+  next =>
+    rw [Nat.modCore.go]
+    split
+    next =>
+      simp only [and_self, ↓reduceIte, *]
+      apply modCore.go.fuel_congr
+    next =>
+      simp only [and_false, ↓reduceIte, *]
+  next =>
+    simp only [false_and, ↓reduceIte, *]
+
 
 @[extern "lean_nat_mod"]
 protected def mod : @& Nat → @& Nat → Nat
   /-
-  Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
-  desirable if trivial `Nat.mod` calculations, namely
+  Nat.modCore is defined with fuel and thus does not reduce with open terms very well.
+  Nevertheless it is desirable for trivial `Nat.mod` calculations, namely
   * `Nat.mod 0 m` for all `m`
-  * `Nat.mod n (m+n)` for concrete literals `n`
-  reduce definitionally.
+  * `Nat.mod n (m+n)` for concrete literals `n`,
+  to reduce definitionally.
   This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
   definition.
    -/
@@ -103,16 +178,16 @@ protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
   show Nat.modCore n m = Nat.mod n m
   match n, m with
   | 0, _ =>
-    rw [Nat.modCore]
+    rw [Nat.modCore_eq]
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
   | (_ + 1), _ =>
     rw [Nat.mod]; dsimp
     refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet
-    rw [Nat.modCore]
+    rw [Nat.modCore_eq]
     exact if_neg fun ⟨_hlt, hle⟩ => h hle
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
-  rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]
+  rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore_eq]
 
 def mod.inductionOn.{u}
       {motive : Nat → Nat → Sort u}