fix: make grind support for ctorIdx debug.grind-safe (#11669)

This PR makes sure that proofs about `ctorIdx` passed to `grind` pass
the `debug.grind` checks, despite reducing a `semireducible` definition.

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

@@ -46,6 +46,8 @@ def propagateCtorIdxUp (e : Expr) : GoalM Unit := e.withApp fun f xs => do
   -- Homogeneous case
   let e' ← shareCommon (mkNatLit conInfo.cidx)
   internalize e' 0
-  pushEq e e' (← mkCongrArg e.appFn! (← mkEqProof a aNode.self))
+  -- We used `mkExpectedPropHint` so that the inferred type of the proof matches the goal,
+  -- to satisfy `debug.grind` checks
+  pushEq e e' (mkExpectedPropHint (← mkCongrArg e.appFn! (← mkEqProof a aNode.self)) (← mkEq e e'))
 
 end Lean.Meta.Grind

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

@@ -1041,7 +1041,7 @@ def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) (splitSource :
     unless (← withGTransparency <| isDefEq (← inferType proof) prop) do
       throwError "`grind` internal error, trying to assert{indentExpr prop}\n\
         with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
-        which is not definitionally equal with `reducible` transparency setting}"
+        which is not definitionally equal with `reducible` transparency setting"
   modify fun s => { s with newRawFacts := s.newRawFacts.enqueue { proof, prop, generation, splitSource } }
 
 /-- Returns the number of theorem instances generated so far. -/
@@ -1198,7 +1198,7 @@ def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
       unless (← withGTransparency <| isDefEq (← inferType proof) expectedType) do
         throwError "`grind` internal error, trying to assert equality{indentExpr expectedType}\n\
             with proof{indentExpr proof}\nwhich has type{indentExpr (← inferType proof)}\n\
-            which is not definitionally equal with `reducible` transparency setting}"
+            which is not definitionally equal with `reducible` transparency setting"
       trace[grind.debug] "pushEqCore: {expectedType}"
   modify fun s => { s with newFacts := s.newFacts.push <| .eq lhs rhs proof isHEq }
 

tests/lean/run/grind_ctorIdx.lean

@@ -1,4 +1,5 @@
 set_option warn.sorry false
+set_option grind.debug true
 
 inductive T where
 | con1 : Nat → T
@@ -6,7 +7,6 @@ inductive T where
 
 opaque double (n : Nat) : T := .con2
 
-
 example (heq_1 : double n = .con1 5) : (double n).ctorIdx = 0 := by
   grind