From 5db865ea2fb678a46a04010eb064d11b718e863f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 14 Dec 2025 15:59:57 +0100
Subject: [PATCH] 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 | 4 +++-
 src/Lean/Meta/Tactic/Grind/Types.lean   | 4 ++--
 tests/lean/run/grind_ctorIdx.lean       | 2 +-
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/CtorIdx.lean b/src/Lean/Meta/Tactic/Grind/CtorIdx.lean
index 02af4da97d..cc67eb8e82 100644
--- a/src/Lean/Meta/Tactic/Grind/CtorIdx.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index c8af42f18c..ca38a4d143 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/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 }
 
diff --git a/tests/lean/run/grind_ctorIdx.lean b/tests/lean/run/grind_ctorIdx.lean
index 8e096f778a..34fb1fdf10 100644
--- a/tests/lean/run/grind_ctorIdx.lean
+++ b/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