From 3857603dbb0b4380322a8ceed0fe097ccf7c607b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 19 Mar 2025 00:08:42 +0100 Subject: [PATCH] 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 ` rather easily.) --- src/Init/Data/Nat/Div/Basic.lean | 109 ++++++++++++++++++++++++++----- 1 file changed, 92 insertions(+), 17 deletions(-) diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean index 94e9bd4d62..555d661014 100644 --- a/src/Init/Data/Nat/Div/Basic.lean +++ b/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}