fix: grind push new fact (#7532)

This PR fixes the procedure for putting new facts into the `grind`
"to-do" list. It ensures the new facts are preprocessed. This PR also
removes some of the clutter in the `Nat.sub` support.

src/Init/Data/Int/Linear.lean

@@ -1658,12 +1658,13 @@ theorem emod_le (x y : Int) (n : Int) : emod_le_cert y n → x % y + n ≤ 0 :=
 theorem natCast_nonneg (x : Nat) : (-1:Int) * NatCast.natCast x ≤ 0 := by
   simp
 
-abbrev natCast_sub_def (x y : Nat) : Int :=
-  if (NatCast.natCast y : Int) + (-1)*NatCast.natCast x ≤ 0 then (NatCast.natCast x : Int) + -1*NatCast.natCast y else (0 : Int)
-
-theorem natCast_sub (x y : Nat) (z : Int)
-    : natCast_sub_def x y = z → (NatCast.natCast (x - y) : Int) = z := by
-  intro; subst z
+theorem natCast_sub (x y : Nat)
+    : (NatCast.natCast (x - y) : Int)
+      =
+      if (NatCast.natCast y : Int) + (-1)*NatCast.natCast x ≤ 0 then
+        (NatCast.natCast x : Int) + -1*NatCast.natCast y
+      else
+        (0 : Int) := by
   show (↑(x - y) : Int) = if (↑y : Int) + (-1)*↑x ≤ 0 then ↑x + (-1)*↑y else 0
   rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
   rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -351,9 +351,9 @@ private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
   modify' fun s => { s with divMod := s.divMod.insert (a, b) }
   let n : Int := 1 - b.natAbs
   let b := mkIntLit b
-  pushNewProof <| mkApp2 (mkConst ``Int.Linear.ediv_emod) a b
-  pushNewProof <| mkApp3 (mkConst ``Int.Linear.emod_nonneg) a b reflBoolTrue
-  pushNewProof <| mkApp4 (mkConst ``Int.Linear.emod_le) a b (toExpr n) reflBoolTrue
+  pushNewFact <| mkApp2 (mkConst ``Int.Linear.ediv_emod) a b
+  pushNewFact <| mkApp3 (mkConst ``Int.Linear.emod_nonneg) a b reflBoolTrue
+  pushNewFact <| mkApp4 (mkConst ``Int.Linear.emod_le) a b (toExpr n) reflBoolTrue
 
 private def propagateDiv (e : Expr) : GoalM Unit := do
   let_expr HDiv.hDiv _ _ _ inst a b ← e | return ()
@@ -373,14 +373,7 @@ private def propagateNatSub (e : Expr) : GoalM Unit := do
   unless (← isInstHSubNat inst) do return ()
   markForeignTerm a .nat
   markForeignTerm b .nat
-  -- TODO: cleanup
-  let aux := mkApp2 (mkConst ``Int.Linear.natCast_sub_def) a b
-  -- TODO: improve `preprocess` to make sure we don't need to unfold manually here
-  let aux ← unfoldReducible aux
-  -- Remark: we preprocess here because we want to propagate `natCast`.
-  -- We don't want to preprocess the whole thing.
-  let r ← preprocess aux
-  pushNewProof <| mkApp4 (mkConst ``Int.Linear.natCast_sub) a b r.expr (← r.getProof)
+  pushNewFact <| mkApp2 (mkConst ``Int.Linear.natCast_sub) a b
 
 /--
 Internalizes an integer (and `Nat`) expression. Here are the different cases that are handled.

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.IntInstTesters
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.Simp
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -24,7 +24,7 @@ def foreignTermOrLit? (e : Expr) : GoalM (Option ForeignType) := do
 private def assertNatCast (e : Expr) : GoalM Unit := do
   let_expr NatCast.natCast _ inst a := e | return ()
   let_expr instNatCastInt := inst | return ()
-  pushNewProof <| mkApp (mkConst ``Int.Linear.natCast_nonneg) a
+  pushNewFact <| mkApp (mkConst ``Int.Linear.natCast_nonneg) a
   markForeignTerm a .nat
 
 private def assertHelpers (e : Expr) : GoalM Unit := do

src/Lean/Meta/Tactic/Grind/Simp.lean

@@ -46,4 +46,15 @@ def preprocess (e : Expr) : GoalM Simp.Result := do
   trace_goal[grind.simp] "{e}\n===>\n{e'}"
   return { r with expr := e' }
 
+/-- Infers the type of the proof, preprocess it, and adds it to todo list. -/
+def pushNewFact (proof : Expr) (generation : Nat := 0) : GoalM Unit := do
+  let prop ← inferType proof
+  let r ← preprocess prop
+  let prop' := r.expr
+  let proof := if let some h := r.proof? then
+    mkApp4 (mkConst ``Eq.mp [levelZero]) prop prop' h proof
+  else
+    proof
+  modify fun s => { s with newFacts := s.newFacts.push <| .fact prop' proof generation }
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -760,21 +760,6 @@ def pushEqBoolTrue (a proof : Expr) : GoalM Unit := do
 def pushEqBoolFalse (a proof : Expr) : GoalM Unit := do
   pushEq a (← getBoolFalseExpr) proof
 
-/--
-Push a new fact into the todo list. This function assumes the fact is in `grind` normal
-form. For facts that need to be preprocessed, use `addNewRawFact` instead.
--/
-def pushNewFact (fact : Expr) (proof : Expr) (generation : Nat := 0) : GoalM Unit := do
-  modify fun s => { s with newFacts := s.newFacts.push <| .fact fact proof generation }
-
-/--
-Infer the type of the proof, and invokes `pushNewFact`. It assumes the type/proposition
-is in `grind` normal form. Only `shareCommon` is used.
--/
-def pushNewProof (proof : Expr) (generation : Nat := 0) : GoalM Unit := do
-  let fact ← shareCommon (← inferType proof)
-  modify fun s => { s with newFacts := s.newFacts.push <| .fact fact proof generation }
-
 /--
 Records that `parent` is a parent of `child`. This function actually stores the
 information in the root (aka canonical representative) of `child`.

tests/lean/run/grind_canon_insts.lean

@@ -59,7 +59,14 @@ def fallback : Fallback := do
 set_option trace.Meta.debug true
 
 /--
-info: [Meta.debug] [-1 * NatCast.natCast (a * (b * c)), -1 * NatCast.natCast (d * (b * c)), a * (b * c), b * c, d * (b * c)]
+info: [Meta.debug] [NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c),
+     NatCast.natCast b * NatCast.natCast c,
+     NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c),
+     -1 * (NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c)),
+     -1 * (NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c)),
+     a * (b * c),
+     b * c,
+     d * (b * c)]
 -/
 #guard_msgs (info) in
 example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by

tests/lean/run/grind_cutsat_div_mod.lean

@@ -26,3 +26,6 @@ example (x y : Int) : x % 2 + y = 3 → x ≤ 5 → x > 4 → y = 1 := by
 
 example (x y : Int) : x = y / 2 → y % 2 = 0 → y - 2*x = 0 := by
   grind
+
+example (x : Int) : x ≥ 0 → (x + 4) / 2 ≤ x + 2 := by
+  grind