fix: make lia and Nat offset simproc proofs cheap to check in the kernel

src/Init/Data/Int/Linear.lean

@@ -51,11 +51,14 @@ attribute [semireducible] Var.denote Expr.denote
 /--
 `Expr.denote` for kernel reduction. Theorems that take user hypotheses state them with
 `Expr.denote_k`, so that the kernel unfolds `Expr.rec` instead of `Expr.denote`'s `brecOn`.
+It is an `abbrev` so that the kernel's lazy delta reduction unfolds it before the user's terms.
 -/
-@[expose] noncomputable def Expr.denote_k (ctx : Context) (e : Expr) : Int :=
+noncomputable abbrev Expr.denote_k (ctx : Context) (e : Expr) : Int :=
   Expr.rec (fun k => k) (fun v => v.denote ctx) (fun _ _ a b => a + b) (fun _ _ a b => a - b)
     (fun _ a => -a) (fun k _ a => k * a) (fun _ k a => a * k) e
 
+attribute [semireducible] Expr.denote_k
+
 @[simp] theorem Expr.denote_k_eq_denote (ctx : Context) (e : Expr) : e.denote_k ctx = e.denote ctx := by
   induction e with
   | num => rfl

src/Init/Data/Nat/Internal/Linear.lean

@@ -536,12 +536,18 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
   simp [Expr.toNormPoly, Poly.norm] at h
   assumption
 
-/-! Kernel-reduction variants for the certificates of `simp +arith` over `Nat`. -/
+/-!
+Kernel-reduction variants for the certificates of `simp +arith` over `Nat`.
+The denotations are `abbrev`s so that the kernel's lazy delta reduction unfolds them before the
+user's terms.
+-/
 
-noncomputable def Expr.denote_k (ctx : Context) (e : Expr) : Nat :=
+noncomputable abbrev Expr.denote_k (ctx : Context) (e : Expr) : Nat :=
   Expr.rec (fun k => k) (fun v => v.denote ctx) (fun _ _ a b => Nat.add a b) (fun k _ a => Nat.mul k a)
     (fun _ k a => Nat.mul a k) e
 
+attribute [semireducible] Expr.denote_k
+
 theorem Expr.denote_k_eq_denote (ctx : Context) (e : Expr) : e.denote_k ctx = e.denote ctx := by
   induction e with
   | num => rfl
@@ -550,9 +556,11 @@ theorem Expr.denote_k_eq_denote (ctx : Context) (e : Expr) : e.denote_k ctx = e.
   | mulL k a ih => show Nat.mul k (a.denote_k ctx) = _; rw [ih]
   | mulR a k ih => show Nat.mul (a.denote_k ctx) k = _; rw [ih]
 
-noncomputable def ExprCnstr.denote_k (ctx : Context) (c : ExprCnstr) : Prop :=
+noncomputable abbrev ExprCnstr.denote_k (ctx : Context) (c : ExprCnstr) : Prop :=
   Bool.rec (c.lhs.denote_k ctx ≤ c.rhs.denote_k ctx) (c.lhs.denote_k ctx = c.rhs.denote_k ctx) c.eq
 
+attribute [semireducible] ExprCnstr.denote_k
+
 theorem ExprCnstr.denote_k_eq_denote (ctx : Context) (c : ExprCnstr) : c.denote_k ctx = c.denote ctx := by
   cases c with
   | mk eq lhs rhs => cases eq <;> simp [denote_k, denote, Expr.denote_k_eq_denote]

src/Init/Data/Nat/Simproc.lean

@@ -45,6 +45,18 @@ theorem add_sub_le (a : Nat) {b c : Nat} (h : b ≤ c) : a + b - c = a - (c - b)
   simp only [Nat.zero_add] at p
   exact p
 
+/-
+Copies of `Nat.add_sub_cancel` and `Nat.add_sub_add_right` for `Nat.reduceSubDiff`. A simproc case
+fires only if its lemma is in the environment, so lemmas from this file keep the simproc off in
+modules that do not import `Init.Data.Nat.Simproc`.
+-/
+
+theorem add_sub_cancel (a b : Nat) : a + b - b = a :=
+  Nat.add_sub_cancel a b
+
+theorem add_sub_add_cancel (a c b : Nat) : a + b - (c + b) = a - c :=
+  Nat.add_sub_add_right a b c
+
 /- Eq proofs -/
 
 theorem add_eq_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b = c) = False :=
@@ -61,6 +73,9 @@ theorem add_eq_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b = c + d) =
 theorem add_eq_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b = c + d) = (a + (b - d) = c) := by
   rw [@Eq.comm _ (a + b) _, add_eq_add_le c a h, @Eq.comm _ _ c]
 
+theorem add_eq_add_cancel (a c b : Nat) : (a + b = c + b) = (a = c) :=
+  propext Nat.add_right_cancel_iff
+
 theorem add_eq_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b = c) = (a = c - b) := by
   have r := add_eq_add_le a 0 h
   simp only [Nat.zero_add] at r
@@ -93,6 +108,9 @@ theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d)
 theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c) := by
   rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]
 
+theorem add_le_add_cancel (a c b : Nat) : (a + b ≤ c + b) = (a ≤ c) :=
+  propext Nat.add_le_add_iff_right
+
 theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b) := by
   have r := add_le_add_le a 0 h
   simp only [Nat.zero_add] at r

src/Init/Grind/Ordered/Linarith.lean

@@ -61,11 +61,15 @@ abbrev Expr.denote {α} [IntModule α] (ctx : Context α) : Expr → α
 /--
 `Expr.denote` for kernel reduction. The theorems that take hypotheses about user terms state them
 with `Expr.denote_k`, so that the kernel unfolds `Expr.rec` instead of `Expr.denote`'s `brecOn`.
+It is an `abbrev` so that the kernel's lazy delta reduction unfolds it before the user's terms.
 -/
-noncomputable def Expr.denote_k {α} [IntModule α] (ctx : Context α) (e : Expr) : α :=
+noncomputable abbrev Expr.denote_k {α} [IntModule α] (ctx : Context α) (e : Expr) : α :=
   Expr.rec 0 (fun v => v.denote ctx) (fun _ _ a b => a + b) (fun _ _ a b => a - b)
     (fun _ a => -a) (fun k _ a => k • a) (fun k _ a => k • a) e
 
+set_option allowUnsafeReducibility true in
+attribute [semireducible] Expr.denote_k
+
 @[simp] theorem Expr.denote_k_eq_denote {α} [IntModule α] (ctx : Context α) (e : Expr) :
     e.denote_k ctx = e.denote ctx := by
   induction e with

src/Init/Grind/Ring/CommSolver.lean

@@ -3230,14 +3230,18 @@ theorem norm_int (ctx : Context Int) (e : Expr) (p : Poly) : norm_int_cert e p 
 /-!
 Kernel-reduction variants of `Poly.denote'`: `cutsat` states the result of `norm_int` with
 `Poly.denote'_k`, which the kernel unfolds to match it with its own polynomials.
+They are `abbrev`s so that the kernel's lazy delta reduction unfolds them before the arithmetic on
+the other side (e.g., `Int.add`), whose unfolding would make the kernel reduce the atoms.
 -/
 
-noncomputable def Mon.denote'_k.go {α} [Semiring α] (ctx : Context α) (m : Mon) : α → α :=
+noncomputable abbrev Mon.denote'_k.go {α} [Semiring α] (ctx : Context α) (m : Mon) : α → α :=
   Mon.rec (fun acc => acc) (fun pw _ ih acc => ih (acc * pw.denote ctx)) m
 
-noncomputable def Mon.denote'_k {α} [Semiring α] (ctx : Context α) (m : Mon) : α :=
+noncomputable abbrev Mon.denote'_k {α} [Semiring α] (ctx : Context α) (m : Mon) : α :=
   Mon.rec 1 (fun pw m _ => Mon.denote'_k.go ctx m (pw.denote ctx)) m
 
+attribute [semireducible] Mon.denote'_k.go Mon.denote'_k
+
 theorem Mon.denote'_k_eq {α} [Semiring α] (ctx : Context α) (m : Mon) : m.denote'_k ctx = m.denote' ctx := by
   have hgo : ∀ m acc, Mon.denote'_k.go ctx m acc = Mon.denote'.go ctx m acc := by
     intro m; induction m with
@@ -3247,21 +3251,25 @@ theorem Mon.denote'_k_eq {α} [Semiring α] (ctx : Context α) (m : Mon) : m.den
   | unit => rfl
   | mult pw m => exact hgo m _
 
-noncomputable def denoteTerm_k {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : α :=
+noncomputable abbrev denoteTerm_k {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : α :=
   Bool.rec (k • Mon.denote'_k ctx m) (Mon.denote'_k ctx m) (Int.beq' k 1)
 
+attribute [semireducible] denoteTerm_k
+
 theorem denoteTerm_k_eq {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : denoteTerm_k ctx k m = denoteTerm ctx k m := by
   unfold denoteTerm_k denoteTerm
   rw [Mon.denote'_k_eq, show Int.beq' k 1 = (k == 1) from by simp [Int.beq'_eq_beq]]
   cases k == 1 <;> rfl
 
-noncomputable def Poly.denote'_k.go {α} [Ring α] (ctx : Context α) (p : Poly) : α → α :=
+noncomputable abbrev Poly.denote'_k.go {α} [Ring α] (ctx : Context α) (p : Poly) : α → α :=
   Poly.rec (fun k acc => Bool.rec (acc + Int.cast k) acc (Int.beqZero_k k))
     (fun k m _ ih acc => ih (acc + denoteTerm_k ctx k m)) p
 
-noncomputable def Poly.denote'_k {α} [Ring α] (ctx : Context α) (p : Poly) : α :=
+noncomputable abbrev Poly.denote'_k {α} [Ring α] (ctx : Context α) (p : Poly) : α :=
   Poly.rec (fun k => Int.cast k) (fun k m p _ => Poly.denote'_k.go ctx p (denoteTerm_k ctx k m)) p
 
+attribute [semireducible] Poly.denote'_k.go Poly.denote'_k
+
 theorem Poly.denote'_k_eq {α} [Ring α] (ctx : Context α) (p : Poly) : p.denote'_k ctx = p.denote' ctx := by
   have hgo : ∀ p acc, Poly.denote'_k.go ctx p acc = Poly.denote'.go ctx p acc := by
     intro p; induction p with

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -255,8 +255,12 @@ private def reduceNatEqExpr (x y : Expr) : SimpM (Option EqResult):= do
       let gtProof ← mkOfDecideEqTrue (mkGTNat yo x)
       applyEqLemma .false ``Nat.Simproc.eq_add_gt #[x, yb, yo, gtProof]
   | .offset xb xo xn, .offset yb yo yn => do
-    if xn ≤ yn then
-      let zb := (if xn = yn then yb else mkAddNat yb (toExpr (yn - xn)))
+    if xn = yn then
+      -- `xo` and `yo` are the same literal. We do not use `add_eq_add_le`: the kernel would have to
+      -- check `yb + (yo - xo) =?= yb`, and it may unfold `yb` instead of `+`.
+      applyEqLemma (.eq xb yb) ``Nat.Simproc.add_eq_add_cancel #[xb, yb, xo]
+    else if xn < yn then
+      let zb := mkAddNat yb (toExpr (yn - xn))
       let leProof ← mkOfDecideEqTrue (mkLENat xo yo)
       applyEqLemma (.eq xb zb) ``Nat.Simproc.add_eq_add_le #[xb, yb, xo, yo, leProof]
     else
@@ -349,8 +353,11 @@ private def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : Simp
       let geProof ← mkOfDecideEqTrue (mkGENat x yo)
       applySimprocConst finExpr ``Nat.Simproc.le_add_ge #[x, yb, yo, geProof]
   | .offset xb xo xn, .offset yb yo yn => do
-    if xn ≤ yn then
-      let finExpr := mkLENat xb (if xn = yn then yb else mkAddNat yb (toExpr (yn - xn)))
+    if xn = yn then
+      -- See `reduceNatEqExpr`.
+      applySimprocConst (mkLENat xb yb) ``Nat.Simproc.add_le_add_cancel #[xb, yb, xo]
+    else if xn < yn then
+      let finExpr := mkLENat xb (mkAddNat yb (toExpr (yn - xn)))
       let leProof ← mkOfDecideEqTrue (mkLENat xo yo)
       applySimprocConst finExpr ``Nat.Simproc.add_le_add_le  #[xb, yb, xo, yo, leProof]
     else
@@ -376,8 +383,11 @@ builtin_simproc [simp, seval] reduceSubDiff ((_ - _ : Nat)) := fun e => do
     let finProof ← Meta.mkEqRefl finExpr
     return .done  { expr := finExpr, proof? := finProof, cache := true }
   | .offset pb po pn, .const n => do
-    if pn ≤ n then
-      let finExpr := if pn = n then pb else mkSubNat pb (toExpr (n - pn))
+    if pn = n then
+      -- See `reduceNatEqExpr`.
+      applySimprocConst pb ``Nat.Simproc.add_sub_cancel #[pb, po]
+    else if pn < n then
+      let finExpr := mkSubNat pb (toExpr (n - pn))
       let leProof ← mkOfDecideEqTrue (mkLENat po q)
       applySimprocConst finExpr ``Nat.Simproc.add_sub_le  #[pb, po, q, leProof]
     else
@@ -388,8 +398,11 @@ builtin_simproc [simp, seval] reduceSubDiff ((_ - _ : Nat)) := fun e => do
       let finExpr := mkSubNat (toExpr (po - nn)) nb
       applySimprocConst finExpr ``Nat.Simproc.sub_add_eq_comm #[p, nb, no]
   | .offset pb po pn, .offset nb no nn => do
-    if pn ≤ nn then
-      let finExpr := mkSubNat pb (if pn = nn then nb else mkAddNat nb (toExpr (nn - pn)))
+    if pn = nn then
+      -- See `reduceNatEqExpr`.
+      applySimprocConst (mkSubNat pb nb) ``Nat.Simproc.add_sub_add_cancel #[pb, nb, po]
+    else if pn < nn then
+      let finExpr := mkSubNat pb (mkAddNat nb (toExpr (nn - pn)))
       let leProof ← mkOfDecideEqTrue (mkLENat po no)
       applySimprocConst finExpr ``Nat.Simproc.add_sub_add_le #[pb, nb, po, no, leProof]
     else

tests/elab/grind_16311.lean

@@ -0,0 +1,21 @@
+set_option maxHeartbeats 0
+set_option maxRecDepth 0
+set_option linter.unusedVariables false
+
+/-!
+Regression test for #16311: the kernel checking of the `lia` proof below did not terminate in
+practice, as it reduced `(2 ^ L - 1 - b) % 2 ^ 32 + (2 ^ 32 - 1)` with unary `Nat` arithmetic.
+-/
+
+theorem V3 (L b record ll A s1 z1 z2 : Nat)
+  (f1 : 1 ≤ L)
+  (f2 : L ≤ 7)
+  (f9 : 2 * 2 ^ (L - 1) ≤ 2 ^ L)
+  (f10 : 2 ^ L ≤ 2 * 2 ^ (L - 1))
+  (f12 : b < 2 ^ (L - 1))
+  (f16 : (2 ^ L - 1 - b) % 2 ^ 32 = 2 ^ L - 1 - b) :
+  ((2 ^ L - 1 - b) % 2 ^ 32 + (2 ^ 32 - 1 % 2 ^ 32)) % 2 ^ 32 + 1 ≤ 2 ^ L := by
+  lia
+
+theorem t (x : Nat) : (x + 1 ≤ (x + 65535) % 65536 + 1) ↔ x ≤ (x + 65535) % 65536 := by
+  simp only [Nat.reduceLeDiff]

tests/elab/grind_cutsat_nat_le.lean.out.expected

@@ -30,9 +30,7 @@
                   (eagerReduce (Eq.refl true))))))
           (Classical.byContradiction
             (Lean.Grind.intro_with_eq (¬x + 1 ≤ 2 * z) (2 * z ≤ x) False
-              (Eq.trans (Nat.not_le_eq (x + 1) (2 * z))
-                (Nat.Simproc.add_le_add_le (2 * z) x (of_decide_eq_true (Eq.refl true))))
-              fun h_2 =>
+              (Eq.trans (Nat.not_le_eq (x + 1) (2 * z)) (Nat.Simproc.add_le_add_cancel (2 * z) x 1)) fun h_2 =>
               id
                 (let ctx :=
                   Lean.RArray.branch 1 (Lean.RArray.leaf ↑x)

tests/elab/grind_kernel_expensive_atoms.lean

@@ -0,0 +1,53 @@
+/-!
+Proofs produced by `lia`, `grind` and the `Nat` offset simprocs must not make the kernel reduce atoms
+such as `(n + 4294967295) % 4294967296`: `Nat.ble` on the `2^32` literals does not terminate in
+practice.
+-/
+
+/-!
+The kernel-reduction denotations of the certificates (`Poly.denote'_k`, `Expr.denote_k`, ...) must
+be unfolded before the arithmetic of the terms they are compared with.
+`Int.Internal.Linear.le_norm_poly` with a `CommRing.norm_int_k` certificate:
+-/
+
+example (x n : Nat) (h : x * x + (n + 4294967295) % 4294967296 ≤ 3)
+    (h' : 5 ≤ (n + 4294967295) % 4294967296) : False := by
+  lia
+
+/-! `Lean.Grind.Linarith.le_norm` states the hypothesis with `Linarith.Expr.denote_k`. -/
+
+example (x y : Rat) (n : Nat) (h : x + (((n + 4294967295) % 4294967296 : Nat) : Rat) ≤ y)
+    (h' : y < x) : False := by
+  grind
+
+/-!
+The `Nat` offset simprocs must not state results that are only definitionally equal to the
+lemma instances when offsets cancel, e.g., `b ≤ c` for `b ≤ c + (1 - 1)`.
+-/
+
+example (x n : Nat) (h : x + 1 ≤ (n + 4294967295) % 4294967296 + 1) :
+    x ≤ (n + 4294967295) % 4294967296 := by
+  simp only [Nat.reduceLeDiff] at h; exact h
+
+example (x n : Nat) (h : x + 1 = (n + 4294967295) % 4294967296 + 1) :
+    x = (n + 4294967295) % 4294967296 := by
+  simp only [Nat.reduceEqDiff] at h; exact h
+
+example (n : Nat) (h : (n + 4294967295) % 4294967296 + 1 - 1 = 0) :
+    (n + 4294967295) % 4294967296 = 0 := by
+  simp only [Nat.reduceSubDiff] at h; exact h
+
+example (x n : Nat) (h : x + 1 - ((n + 4294967295) % 4294967296 + 1) = 0) :
+    x - (n + 4294967295) % 4294967296 = 0 := by
+  simp only [Nat.reduceSubDiff] at h; exact h
+
+example (x n : Nat) (h : x + 1 ≤ (n + 4294967295) % 4294967296 + 1) :
+    x ≤ (n + 4294967295) % 4294967296 := by
+  lia
+
+/-! Both issues. -/
+
+theorem pow_mod (L b : Nat) (f9 : 2 * 2 ^ (L - 1) ≤ 2 ^ L) (f10 : 2 ^ L ≤ 2 * 2 ^ (L - 1))
+    (f12 : b < 2 ^ (L - 1)) (f16 : (2 ^ L - 1 - b) % 2 ^ 32 = 2 ^ L - 1 - b) :
+    ((2 ^ L - 1 - b) % 2 ^ 32 + (2 ^ 32 - 1 % 2 ^ 32)) % 2 ^ 32 + 1 ≤ 2 ^ L := by
+  lia