fix: shareCommon issues in grind (#7834)

This PR fixes some of the `shareCommon` issues in `grind`.

src/Lean/Meta/Tactic/Grind.lean

@@ -73,5 +73,6 @@ builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse
 builtin_initialize registerTraceClass `grind.debug.mbtc
 builtin_initialize registerTraceClass `grind.debug.ematch
 builtin_initialize registerTraceClass `grind.debug.proveEq
+builtin_initialize registerTraceClass `grind.debug.pushNewFact
 
 end Lean

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

@@ -66,5 +66,6 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.nat
 builtin_initialize registerTraceClass `grind.debug.cutsat.proof
 builtin_initialize registerTraceClass `grind.debug.cutsat.internalize
 builtin_initialize registerTraceClass `grind.debug.cutsat.markTerm
+builtin_initialize registerTraceClass `grind.debug.cutsat.natCast
 
 end Lean

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

@@ -106,7 +106,7 @@ def propagateNatDvd (e : Expr) : GoalM Unit := do
   let some (d, b) ← Int.OfNat.toIntDvd? e | return ()
   let gen ← getGeneration e
   let ctx ← getForeignVars .nat
-  let b' ← toLinearExpr (b.denoteAsIntExpr ctx) gen
+  let b' ← toLinearExpr (← b.denoteAsIntExpr ctx) gen
   let p := b'.norm
   if (← isEqTrue e) then
     let c := { d, p, h := .coreNat e d b b' : DvdCnstr }

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

@@ -243,8 +243,8 @@ private def processNewNatEq (a b : Expr) : GoalM Unit := do
   let (lhs, rhs) ← Int.OfNat.toIntEq a b
   let gen ← getGeneration a
   let ctx ← getForeignVars .nat
-  let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen
-  let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen
+  let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen
+  let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
   let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : EqCnstr }
   trace[grind.debug.cutsat.nat] "{← c.pp}"
@@ -290,8 +290,8 @@ private def processNewNatDiseq (a b : Expr) : GoalM Unit := do
   let (lhs, rhs) ← Int.OfNat.toIntEq a b
   let gen ← getGeneration a
   let ctx ← getForeignVars .nat
-  let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen
-  let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen
+  let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen
+  let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
   let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : DiseqCnstr }
   trace[grind.debug.cutsat.nat] "{← c.pp}"

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

@@ -31,6 +31,9 @@ def mkForeignVar (e : Expr) (t : ForeignType) : GoalM Var := do
 def foreignTerm? (e : Expr) : GoalM (Option ForeignType) := do
   return (·.2) <$> (← get').foreignVarMap.find? { expr := e }
 
+def hasForeignVar (e : Expr) : GoalM Bool :=
+  return (← get').foreignVarMap.contains { expr := e }
+
 def foreignTermOrLit? (e : Expr) : GoalM (Option ForeignType) := do
   if isNatNum e then return some .nat
   foreignTerm? e

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

@@ -152,8 +152,8 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   let some (lhs, rhs) ← Int.OfNat.toIntLe? e | return ()
   let gen ← getGeneration e
   let ctx ← getForeignVars .nat
-  let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen
-  let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen
+  let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen
+  let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
   trace[grind.debug.cutsat.nat] "{← p.pp}"
   let c ← if eqTrue then

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

@@ -27,20 +27,23 @@ instance : ToExpr OfNat.Expr where
   toExpr a := OfNat.toExpr a
   toTypeExpr := mkConst ``OfNat.Expr
 
-def Expr.denoteAsIntExpr (ctx : PArray Lean.Expr) (e : Expr) : Lean.Expr :=
-  match e with
-  | .num v    => mkIntLit v
-  | .var i    => mkIntNatCast ctx[i]!
-  | .add a b  => mkIntAdd (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b)
-  | .mul a b  => mkIntMul (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b)
-  | .div a b  => mkIntDiv (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b)
-  | .mod a b  => mkIntMod (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b)
-
 open Lean.Meta.Grind
 open Lean.Meta.Grind.Arith.Cutsat
 
 open Meta
 
+def Expr.denoteAsIntExpr (ctx : PArray Lean.Expr) (e : Expr) : GoalM Lean.Expr :=
+  shareCommon (go e)
+where
+  go (e : Expr) : Lean.Expr :=
+    match e with
+    | .num v    => mkIntLit v
+    | .var i    => mkIntNatCast ctx[i]!
+    | .add a b  => mkIntAdd (go a) (go b)
+    | .mul a b  => mkIntMul (go a) (go b)
+    | .div a b  => mkIntDiv (go a) (go b)
+    | .mod a b  => mkIntMod (go a) (go b)
+
 partial def toOfNatExpr (e : Lean.Expr) : GoalM Expr := do
   let mkVar (e : Lean.Expr) : GoalM Expr := do
     let x ← mkForeignVar e .nat
@@ -125,13 +128,13 @@ namespace Lean.Meta.Grind.Arith.Cutsat
 If `e` is of the form `a.denoteAsInt ctx` for some `a` and `ctx`,
 assert that `e` is nonnegative.
 -/
-def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := do
+def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := withIncRecDepth do
   if e.isAppOf ``NatCast.natCast then return ()
   let some rhs ← Int.OfNat.ofDenoteAsIntExpr? e |>.run | return ()
   let gen ← getGeneration e
   let ctx ← getForeignVars .nat
   let lhs' : Int.Linear.Expr := .num 0
-  let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen
+  let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
   trace[grind.debug.cutsat.nat] "{← p.pp}"
   let c := { p, h := .denoteAsIntNonneg rhs rhs' : LeCnstr }

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

@@ -16,10 +16,10 @@ and these expressions must be normalized inside of the cutsat module.
 /-- Converts the given integer expression into `Int.Linear.Expr` -/
 partial def toLinearExpr (e : Expr) (generation : Nat := 0) : GoalM Int.Linear.Expr := do
   let toVar (e : Expr) := do
+    let e ← shareCommon e
     if (← alreadyInternalized e) then
       return .var (← mkVar e)
     else
-      let e ← shareCommon e
       internalize e generation
       return .var (← mkVar e)
   let mul (a b : Expr) := do

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

@@ -14,6 +14,7 @@ namespace Lean.Meta.Grind.Arith.Cutsat
 private def assertNatCast (e : Expr) : GoalM Unit := do
   let_expr NatCast.natCast _ inst a := e | return ()
   let_expr instNatCastInt := inst | return ()
+  trace[grind.debug.cutsat.natCast] "{a}"
   pushNewFact <| mkApp (mkConst ``Int.Linear.natCast_nonneg) a
   discard <| mkForeignVar a .nat
 

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

@@ -53,12 +53,14 @@ def pushNewFact' (prop : Expr) (proof : Expr) (generation : Nat := 0) : GoalM Un
     mkApp4 (mkConst ``Eq.mp [levelZero]) prop prop' h proof
   else
     proof
+  trace[grind.debug.pushNewFact] "{prop} ==> {prop'}"
   modify fun s => { s with newFacts := s.newFacts.push <| .fact prop' proof generation }
 
 
 /-- 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
+  trace[grind.debug.pushNewFact] "{prop}"
   pushNewFact' prop proof generation
 
 end Lean.Meta.Grind