fix: markNestedProofs (#7355)

This PR fixes a bug in the `markNestedProofs` preprocessor used in the
`grind` tactic.

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

@@ -8,6 +8,7 @@ import Init.Grind.Util
 import Lean.Util.PtrSet
 import Lean.Meta.Basic
 import Lean.Meta.InferType
+import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind
 
@@ -21,6 +22,13 @@ where
       if let some r := (← get).find? e then
         return r
       let prop ← inferType e
+      /-
+      We must unfold reducible constants occurring in `prop` because the congruence closure
+      module in `grind` assumes they have been expanded.
+      See `grind_mark_nested_proofs_bug.lean` for an example.
+      TODO: We may have to normalize `prop` too.
+      -/
+      let prop ← unfoldReducible prop
       let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
       modify fun s => s.insert e e'
       return e'

tests/lean/run/grind_mark_nested_proofs_bug.lean

@@ -0,0 +1,28 @@
+set_option grind.warning false
+
+example (as bs cs : Array α) (v : α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        (h₃ : cs = bs)
+        (h₄ : i ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  skip
+  grind only [= Array.getElem_set_ne, = Array.size_set] -- works
+
+theorem Array.getElem_set_ne_abstracted (xs : Array α) (i : Nat) (h' : i < xs.size) (v : α) {j : Nat}
+    (pj : j < xs.size) (h : i ≠ j) :
+    (xs.set i v)[j]'(by as_aux_lemma => simp [*]) = xs[j] := Array.getElem_set_ne xs i h' v pj h
+
+example (as bs cs : Array α) (v : α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        (h₃ : cs = bs)
+        (h₄ : i ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind only [= Array.getElem_set_ne_abstracted, = Array.size_set] -- should work