feat: create a let-expression for storing the context in cutsat proofs (#7139)

This PR uses a `let`-expression for storing the (shared) context in
proofs produced by the cutsat procedure in `grind`.

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

@@ -36,12 +36,13 @@ partial def assertDvdCnstr (cₚ : DvdCnstrWithProof) : GoalM Unit := withIncRec
   let cₚ ← cₚ.norm
   if cₚ.isUnsat then
     trace[grind.cutsat.dvd.unsat] "{← cₚ.denoteExpr}"
-    withProofContext do
+    let hf ← withProofContext do
       let h ← cₚ.toExprProof
       let heq := mkApp3 (mkConst ``Int.Linear.DvdCnstr.eq_false_of_isUnsat) (← getContext) (toExpr cₚ.c) reflBoolTrue
       let c ← cₚ.denoteExpr
       let heq ← mkExpectedTypeHint heq (← mkEq c (← getFalseExpr))
-      closeGoal (← mkEqMP heq h)
+      mkEqMP heq h
+    closeGoal hf
   else if cₚ.isTrivial then
     trace[grind.cutsat.dvd.trivial] "{← cₚ.denoteExpr}"
     return ()

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

@@ -92,7 +92,9 @@ abbrev caching (id : Nat) (k : ProofM Expr) : ProofM Expr := do
 abbrev DvdCnstrWithProof.caching (c : DvdCnstrWithProof) (k : ProofM Expr) : ProofM Expr :=
   Cutsat.caching c.id k
 
-abbrev withProofContext (x : ProofM α) : GoalM α := do
-  x (← toContextExpr) |>.run' {}
+abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
+  withLetDecl `ctx (mkApp (mkConst ``RArray) (mkConst ``Int)) (← toContextExpr) fun ctx => do
+    let h ← x ctx |>.run' {}
+    mkLetFVars #[ctx] h
 
 end Lean.Meta.Grind.Arith.Cutsat

tests/lean/run/grind_cutsat_div_1.lean

@@ -11,6 +11,10 @@ theorem ex₂ (a b : Int) (h₀ : 2 ∣ a + 1) (h₁ : 2 ∣ b + a) (h₂ : 2
 theorem ex₃ (a b : Int) (_ : 2 ∣ a + 1) (h₁ : 3 ∣ a + 3*b + a) (h₂ : 2 ∣ 3*b + a + 3 - b) (h₃ : 3 ∣ 3 * b + 2 * a + 1) : False := by
   grind
 
+theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3 ∣ f (f a) + 3*b + f (f a)) (h₂ : 2 ∣ 3*b + f (f a) + 3 - b) (h₃ : 3 ∣ 3 * b + 2 * f (f a) + 1) : False := by
+  grind
+
 #print ex₁
 #print ex₂
 #print ex₃
+#print ex₄