chore: fix tests

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

@@ -45,7 +45,7 @@ def propagateBetaEqs (lams : Array Expr) (f : Expr) (args : Array Expr) : GoalM
           h ← mkCongrFun h arg
         let eq ← mkEq lhs rhs
         trace_goal[grind.beta] "{eq}, using {lam}"
-        addNewRawFact h eq (gen+1)
+        addNewRawFact h eq (gen+1) (.beta lam)
 
 private def isPropagateBetaTarget (e : Expr) : GoalM Bool := do
   let .app f _ := e | return false

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

@@ -36,6 +36,6 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
     reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
     return ()
   trace[grind.ext] "{thm.declName}: {prop'}"
-  addNewRawFact proof' prop' ((← getGeneration e) + 1)
+  addNewRawFact proof' prop' ((← getGeneration e) + 1) (.ext thm.declName)
 
 end Lean.Meta.Grind

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

@@ -94,7 +94,7 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       let u ← getLevel α
       let prop := mkApp2 (mkConst ``Exists [u]) α (mkLambda n bi α (mkNot p))
       let proof := mkApp3 (mkConst ``Grind.of_forall_eq_false [u]) α (mkLambda n bi α p) (← mkEqFalseProof e)
-      addNewRawFact proof prop (← getGeneration e)
+      addNewRawFact proof prop (← getGeneration e) (.forallProp e)
     else
       let h ← mkEqFalseProof e
       pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
@@ -104,7 +104,7 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       trace_goal[grind.eqResolution] "{e}, {e'}"
       let h := mkOfEqTrueCore e (← mkEqTrueProof e)
       let h' := mkApp h' h
-      addNewRawFact h' e' (← getGeneration e)
+      addNewRawFact h' e' (← getGeneration e) (.forallProp e)
     else
       if b.hasLooseBVars then
         addLocalEMatchTheorems e
@@ -121,6 +121,6 @@ builtin_grind_propagator propagateExistsDown ↓Exists := fun e => do
     let notP := mkApp (mkConst ``Not) (mkApp p (.bvar 0) |>.headBeta)
     let prop := mkForall `x .default α notP
     let proof := mkApp3 (mkConst ``forall_not_of_not_exists u) α p (mkOfEqFalseCore e (← mkEqFalseProof e))
-    addNewRawFact proof prop (← getGeneration e)
+    addNewRawFact proof prop (← getGeneration e) (.existsProp e)
 
 end Lean.Meta.Grind

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

@@ -59,15 +59,21 @@ def isMorallyIff (e : Expr) : Bool :=
   let_expr Eq α _ _ := e | false
   α.isProp
 
+private def mkDefaultSplitInfo (e : Expr) : GrindM SplitInfo :=
+  return .default e (← readThe Context).splitSource
+
+private def addDefaultSplitCandidate (e : Expr) : GoalM Unit := do
+  addSplitCandidate (← mkDefaultSplitInfo e)
+
 /-- Inserts `e` into the list of case-split candidates if applicable. -/
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   match h : e with
   | .app .. =>
     if (← getConfig).splitIte && (isIte e || isDIte e) then
-      addSplitCandidate (.default e)
+      addDefaultSplitCandidate e
       return ()
     if isMorallyIff e then
-      addSplitCandidate (.default e)
+      addDefaultSplitCandidate e
       return ()
     if (← getConfig).splitMatch then
       if (← isMatcherApp e) then
@@ -76,7 +82,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
           -- and consequently don't need to be split.
           return ()
         else
-          addSplitCandidate (.default e)
+          addDefaultSplitCandidate e
           return ()
     let .const declName _  := e.getAppFn | return ()
       if forbiddenSplitTypes.contains declName then
@@ -84,24 +90,25 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       unless (← isInductivePredicate declName) do
         return ()
       if (← get).split.casesTypes.isSplit declName then
-        addSplitCandidate (.default e)
+        addDefaultSplitCandidate e
       else if (← getConfig).splitIndPred then
-        addSplitCandidate (.default e)
+        addDefaultSplitCandidate e
   | .fvar .. =>
     let .const declName _ := (← whnf (← inferType e)).getAppFn | return ()
     if (← get).split.casesTypes.isSplit declName then
-      addSplitCandidate (.default e)
+      addDefaultSplitCandidate e
   | .forallE _ d _ _ =>
+    let currSplitSource := (← readThe Context).splitSource
     if (← getConfig).splitImp then
       if (← isProp d) then
-        addSplitCandidate (.imp e (h ▸ rfl))
+        addSplitCandidate (.imp e (h ▸ rfl) currSplitSource)
     else if Arith.isRelevantPred d then
       -- TODO: should we keep lookahead after we implement non-chronological backtracking?
       if (← getConfig).lookahead then
-        addLookaheadCandidate (.imp e (h ▸ rfl))
+        addLookaheadCandidate (.imp e (h ▸ rfl) currSplitSource)
       -- We used to add the `split` only if `lookahead := false`, but it was counterintuitive
       -- to make `grind` "stronger" by disabling a feature.
-      addSplitCandidate (.imp e (h ▸ rfl))
+      addSplitCandidate (.imp e (h ▸ rfl) currSplitSource)
   | _ => pure ()
 
 /--
@@ -273,7 +280,8 @@ where
         -- if (← getConfig).lookahead then
         --   addLookaheadCandidate (.arg other.app parent i eq)
         -- else
-        addSplitCandidate (.arg other.app parent i eq)
+        let currSplitSource := (← readThe Context).splitSource
+        addSplitCandidate (.arg other.app parent i eq currSplitSource)
     modify fun s => { s with split.argsAt := s.split.argsAt.insert (f, i) ({ arg, type, app := parent } :: others) }
     return ()
 

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

@@ -258,7 +258,7 @@ def intros' (generation : Nat) : SearchM Bool := do
   return true
 
 /-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
-def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : SearchM Unit := do
+private def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : SearchM Unit := do
   if isEagerCasesCandidate (← getGoal) prop then
     let goal ← getGoal
     let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
@@ -280,8 +280,10 @@ def assertNext : SearchM Bool := do
   let some (fact, newRawFacts) := goal.newRawFacts.dequeue?
     | return false
   setGoal { goal with newRawFacts }
-  assertAt fact.proof fact.prop fact.generation
-  return true
+  withSplitSource fact.splitSource do
+    -- Remark: we should probably add `withGeneration`
+    assertAt fact.proof fact.prop fact.generation
+    return true
 
 /--
 Asserts all facts in the `goal` fact queue.

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

@@ -45,7 +45,7 @@ private def mkCandidate (a b : ArgInfo) (i : Nat) : GoalM SplitInfo := do
     (b.arg, a.arg)
   let eq ← mkEq lhs rhs
   let eq ← shareCommon (← canon eq)
-  return .arg a.app b.app i eq
+  return .arg a.app b.app i eq (.mbtc a.app b.app i)
 
 /-- Model-based theory combination. -/
 def mbtc (ctx : MBTC.Context) : GoalM Bool := do
@@ -84,7 +84,7 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do
   let result ← result.filterMapM fun info => do
     if (← isKnownCaseSplit info) then
       return none
-    let .arg a b _ eq := info | return none
+    let .arg a b _ eq _ := info | return none
     internalize eq (Nat.max (← getGeneration a) (← getGeneration b))
     return some info
   if result.isEmpty then

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

@@ -125,10 +125,13 @@ private def splitDiagInfoToMessageData (ss : Array SplitDiagInfo) : MetaM Messag
   let mctx ← getMCtx
   let opts ← getOptions
   let cls := `split
-  let data ← ss.mapM fun { c, lctx, numCases, .. } => do
-    let m := m!"[{numCases}] {c}"
-    let m := MessageData.withContext { env, mctx, lctx, opts } m
-    return .trace { cls } m #[]
+  let data ← ss.mapM fun { c, lctx, numCases, gen, splitSource } => do
+    let header := m!"{c}"
+    return MessageData.withContext { env, mctx, lctx, opts } <| .trace { cls } header #[
+      .trace { cls } m!"source: {← splitSource.toMessageData}" #[],
+      .trace { cls } m!"generation: {gen}" #[],
+      .trace { cls } m!"# cases: {numCases}" #[]
+    ]
   return .trace { cls } "Case splits" data
 
 -- Diagnostics information for the whole search

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

@@ -172,8 +172,10 @@ private def ppCasesTrace : M Unit := do
   let goal ← read
   unless goal.split.trace.isEmpty do
     let mut msgs := #[]
-    for { expr, i , num } in goal.split.trace.reverse do
-      msgs := msgs.push <| .trace { cls := `cases } m!"[{i+1}/{num}]: {expr}" #[]
+    for { expr, i , num, source } in goal.split.trace.reverse do
+      msgs := msgs.push <| .trace { cls := `cases } m!"[{i+1}/{num}]: {expr}" #[
+        .trace { cls := `cases } m!"source: {← source.toMessageData}" #[]
+      ]
     pushMsg <| .trace { cls := `cases } "Case analyses" msgs
 
 def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do

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

@@ -156,9 +156,9 @@ private def checkForallStatus (imp : Expr) (h : imp.isForall) : GoalM SplitStatu
 
 def checkSplitStatus (s : SplitInfo) : GoalM SplitStatus := do
   match s with
-  | .default e => checkDefaultSplitStatus e
-  | .imp e h => checkForallStatus e h
-  | .arg a b _ eq => checkSplitInfoArgStatus a b eq
+  | .default e _    => checkDefaultSplitStatus e
+  | .imp e h _      => checkForallStatus e h
+  | .arg a b _ eq _ => checkSplitInfoArgStatus a b eq
 
 private inductive SplitCandidate where
   | none
@@ -249,11 +249,11 @@ def splitNext : SearchM Bool := withCurrGoalContext do
   let cExpr := c.getExpr
   let gen ← getGeneration cExpr
   let genNew := if numCases > 1 || isRec then gen+1 else gen
-  saveSplitDiagInfo cExpr genNew numCases
+  saveSplitDiagInfo cExpr genNew numCases c.source
   markCaseSplitAsResolved cExpr
   trace_goal[grind.split] "{cExpr}, generation: {gen}"
   let mvarId ← mkAuxMVarForCurrGoal
-  let mvarIds ← if let .imp e h := c then
+  let mvarIds ← if let .imp e h _ := c then
     casesWithTrace mvarId (mkGrindEM (e.forallDomain h))
   else if (← isMatcherApp cExpr) then
     casesMatch mvarId cExpr
@@ -263,7 +263,7 @@ def splitNext : SearchM Bool := withCurrGoalContext do
   let numSubgoals := mvarIds.length
   let goals := mvarIds.mapIdx fun i mvarId => { goal with
     mvarId
-    split.trace := { expr := cExpr, i, num := numSubgoals } :: goal.split.trace
+    split.trace := { expr := cExpr, i, num := numSubgoals, source := c.source } :: goal.split.trace
   }
   mkChoice (mkMVar mvarId) goals genNew
   intros genNew

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

@@ -53,6 +53,36 @@ register_builtin_option grind.warning : Bool := {
   descr    := "disable `grind` usage warning"
 }
 
+/--
+Case-split source. That is, where it came from.
+We store the current source in the `grind` context.
+-/
+inductive SplitSource where
+  | /-- Generated while instantiating a theorem using E-matching. -/
+    ematch (origin : Origin)
+  | /-- Generated while instantiating an extensionality theorem with name `declName` -/
+    ext (declName : Name)
+  | /-- Model-based theory combination equality coming from the i-th argument of applications `a` and `b` -/
+    mbtc (a b : Expr) (i : Nat)
+  | /-- Beta-reduction. -/
+    beta (e : Expr)
+  | /-- Forall-propagator. -/
+    forallProp (e : Expr)
+  | /-- Exists-propagator. -/
+    existsProp (e : Expr)
+  | /-- Input goal -/
+    input
+  deriving Inhabited
+
+def SplitSource.toMessageData : SplitSource → MetaM MessageData
+  | .ematch origin => return m!"E-matching {← origin.pp}"
+  | .ext declName => return m!"Extensionality {declName}"
+  | .mbtc a b i => return m!"Model-based theory combination at argument #{i} of{indentExpr a}\nand{indentExpr b}"
+  | .beta e => return m!"Beta-reduction of{indentExpr e}"
+  | .forallProp e => return m!"Forall propagation at{indentExpr e}"
+  | .existsProp e => return m!"Exists propagation at{indentExpr e}"
+  | .input => return m!"Initial goal"
+
 /-- Context for `GrindM` monad. -/
 structure Context where
   simp         : Simp.Context
@@ -74,11 +104,13 @@ structure Context where
   user with "false-alarms". If the instantiation fails, we produce a more informative issue anyways.
   -/
   reportMVarIssue : Bool := true
-  trueExpr   : Expr
-  falseExpr  : Expr
-  natZExpr   : Expr
-  btrueExpr  : Expr
-  bfalseExpr : Expr
+  /-- Current source of case-splits. -/
+  splitSource  : SplitSource := .input
+  trueExpr     : Expr
+  falseExpr    : Expr
+  natZExpr     : Expr
+  btrueExpr    : Expr
+  bfalseExpr   : Expr
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -123,10 +155,11 @@ private def emptySC : ShareCommon.State.{0} ShareCommon.objectFactory := ShareCo
 
 /-- Case-split diagnostic information -/
 structure SplitDiagInfo where
-  lctx     : LocalContext
-  c        : Expr
-  gen      : Nat
-  numCases : Nat
+  lctx        : LocalContext
+  c           : Expr
+  gen         : Nat
+  numCases    : Nat
+  splitSource : SplitSource
 
 /-- State for the `GrindM` monad. -/
 structure State where
@@ -172,6 +205,13 @@ See comment at `Grind.Context.reportMVarIssue` for additional details.
 def withoutReportingMVarIssues [MonadControlT GrindM m] [Monad m] : m α → m α :=
   mapGrindM <| withTheReader Grind.Context fun ctx => { ctx with reportMVarIssue := false }
 
+/--
+`withSplitSource s x` executes `x` and uses `s` as the split source for any case-split
+registered.
+-/
+def withSplitSource [MonadControlT GrindM m] [Monad m] (splitSource : SplitSource) : m α → m α :=
+  mapGrindM <| withTheReader Grind.Context fun ctx => { ctx with splitSource }
+
 /-- Returns the user-defined configuration options -/
 def getConfig : GrindM Grind.Config :=
   return (← readThe Context).config
@@ -214,7 +254,7 @@ private def incCounter [Hashable α] [BEq α] (s : PHashMap α Nat) (k : α) : P
     else
       s.insert k 1
 
-def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
+private def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
   if (← getConfig).trace then
     unless (← isMatchEqLikeDeclName thm.origin.key) do
       modify fun s => { s with trace.thms := s.trace.thms.insert { origin := thm.origin, kind := thm.kind } }
@@ -233,10 +273,10 @@ def saveAppOf (h : HeadIndex) : GrindM Unit := do
     let .const declName := h | return ()
     modify fun s => { s with counters.apps := incCounter s.counters.apps declName }
 
-def saveSplitDiagInfo (c : Expr) (gen : Nat) (numCases : Nat) : GrindM Unit := do
+def saveSplitDiagInfo (c : Expr) (gen : Nat) (numCases : Nat) (splitSource : SplitSource) : GrindM Unit := do
   if (← isDiagnosticsEnabled) then
     let lctx ← getLCtx
-    modify fun s => { s with splitDiags := s.splitDiags.push { c, gen, lctx, numCases } }
+    modify fun s => { s with splitDiags := s.splitDiags.push { c, gen, lctx, numCases, splitSource } }
 
 @[inline] def getMethodsRef : GrindM MethodsRef :=
   read
@@ -495,9 +535,11 @@ abbrev PreInstanceSet := PHashSet PreInstance
 
 /-- New raw fact to be preprocessed, and then asserted. -/
 structure NewRawFact where
-  proof      : Expr
-  prop       : Expr
-  generation : Nat
+  proof        : Expr
+  prop         : Expr
+  generation   : Nat
+  /-- `splitSource` to use when internalizing this fact. -/
+  splitSource  : SplitSource
   deriving Inhabited
 
 /-- Canonicalizer state. See `Canon.lean` for additional details. -/
@@ -509,9 +551,10 @@ structure Canon.State where
 
 /-- Trace information for a case split. -/
 structure CaseTrace where
-  expr : Expr
-  i    : Nat
-  num  : Nat
+  expr   : Expr
+  i      : Nat
+  num    : Nat
+  source : SplitSource
   deriving Inhabited
 
 /-- E-matching related fields for the `grind` goal. -/
@@ -544,38 +587,51 @@ inductive SplitInfo where
   | /--
     Term `e` may be an inductive predicate, `match`-expression, `if`-expression, implication, etc.
     -/
-    default (e : Expr)
+    default (e : Expr) (source : SplitSource)
   /-- `e` is an implication and we want to split on its antecedent. -/
-  | imp (e : Expr) (h : e.isForall)
+  | imp (e : Expr) (h : e.isForall) (source : SplitSource)
   | /--
     Given applications `a` and `b`, case-split on whether the corresponding
     `i`-th arguments are equal or not. The split is only performed if all other
     arguments are already known to be equal or are also tagged as split candidates.
     -/
-    arg (a b : Expr) (i : Nat) (eq : Expr)
-  deriving Hashable, Inhabited
+    arg (a b : Expr) (i : Nat) (eq : Expr) (source :SplitSource)
+  deriving Inhabited
+
+protected def SplitInfo.hash : SplitInfo → UInt64
+ | .default e _ => hash e
+ | .imp e _ _   => hash e
+ | .arg _ _ _ e _ => hash e
+
+instance : Hashable SplitInfo where
+  hash := SplitInfo.hash
 
 def SplitInfo.beq : SplitInfo → SplitInfo → Bool
- | .default e₁, .default e₂ => e₁ == e₂
- | .imp e₁ _, .imp e₂ _ => e₁ == e₂
- | .arg a₁ b₁ i₁ eq₁, arg a₂ b₂ i₂ eq₂ => a₁ == a₂ && b₁ == b₂ && i₁ == i₂ && eq₁ == eq₂
+ | .default e₁ _, .default e₂ _ => e₁ == e₂
+ | .imp e₁ _ _, .imp e₂ _ _=> e₁ == e₂
+ | .arg a₁ b₁ i₁ eq₁ _, arg a₂ b₂ i₂ eq₂ _ => a₁ == a₂ && b₁ == b₂ && i₁ == i₂ && eq₁ == eq₂
  | _, _ => false
 
 instance : BEq SplitInfo where
   beq := SplitInfo.beq
 
 def SplitInfo.getExpr : SplitInfo → Expr
-  | .default e => e
-  | .imp e h => e.forallDomain h
-  | .arg _ _ _ eq => eq
+  | .default e _ => e
+  | .imp e h _ => e.forallDomain h
+  | .arg _ _ _ eq _ => eq
+
+def SplitInfo.source : SplitInfo → SplitSource
+  | .default _ s   => s
+  | .imp _ _ s     => s
+  | .arg _ _ _ _ s => s
 
 def SplitInfo.lt : SplitInfo → SplitInfo → Bool
-  | .default e₁, .default e₂     => e₁.lt e₂
-  | .imp e₁ _, .imp e₂ _         => e₁.lt e₂
-  | .arg _ _ _ e₁, .arg _ _ _ e₂ => e₁.lt e₂
-  | .default .., _               => true
-  | .imp .., _                   => true
-  | _, _                         => false
+  | .default e₁ _, .default e₂ _     => e₁.lt e₂
+  | .imp e₁ _ _, .imp e₂ _ _         => e₁.lt e₂
+  | .arg _ _ _ e₁ _, .arg _ _ _ e₂ _ => e₁.lt e₂
+  | .default .., _                   => true
+  | .imp .., _                       => true
+  | _, _                             => false
 
 /-- Argument `arg : type` of an application `app` in `SplitInfo`. -/
 structure SplitArg where
@@ -713,18 +769,18 @@ def markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool :=
   return true
 
 /-- Adds a new fact `prop` with proof `proof` to the queue for preprocessing and the assertion. -/
-def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
+def addNewRawFact (proof : Expr) (prop : Expr) (generation : Nat) (splitSource : SplitSource) : GoalM Unit := do
   if grind.debug.get (← getOptions) then
     unless (← withReducible <| 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}"
-  modify fun s => { s with newRawFacts := s.newRawFacts.enqueue { proof, prop, generation } }
+  modify fun s => { s with newRawFacts := s.newRawFacts.enqueue { proof, prop, generation, splitSource } }
 
 /-- Adds a new theorem instance produced using E-matching. -/
 def addTheoremInstance (thm : EMatchTheorem) (proof : Expr) (prop : Expr) (generation : Nat) : GoalM Unit := do
   saveEMatchTheorem thm
-  addNewRawFact proof prop generation
+  addNewRawFact proof prop generation (.ematch thm.origin)
   modify fun s => { s with ematch.numInstances := s.ematch.numInstances + 1 }
 
 /-- Returns `true` if the maximum number of instances has been reached. -/
@@ -1355,7 +1411,7 @@ def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
     modify fun s => { s with split.resolved := s.split.resolved.insert { expr := e } }
 
 private def updateSplitArgPosMap (sinfo : SplitInfo) : GoalM Unit := do
-  let .arg a b i _ := sinfo | return ()
+  let .arg a b i _ _ := sinfo | return ()
   let key := (a, b)
   let is := (← get).split.argPosMap[key]? |>.getD []
   modify fun s => { s with

tests/lean/run/grind_pre.lean

@@ -161,6 +161,7 @@ right : r
     [prop] r
   [cases] Case analyses
     [cases] [1/2]: p = r
+      [cases] source: Initial goal
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by

tests/lean/run/grind_split_issue.lean

@@ -25,6 +25,7 @@ h_1 : ⋯ ≍ ⋯
     [eqc] {s, 0}
   [cases] Case analyses
     [cases] [1/2]: X c 0
+      [cases] source: Initial goal
   [cutsat] Assignment satisfying linear constraints
     [assign] c := 1
     [assign] s := 0