fix: case splitting on data

src/Lean/Meta/Tactic/Grind.lean

@@ -75,5 +75,6 @@ builtin_initialize registerTraceClass `grind.debug.beta
 builtin_initialize registerTraceClass `grind.debug.internalize
 builtin_initialize registerTraceClass `grind.debug.matchCond
 builtin_initialize registerTraceClass `grind.debug.matchCond.lambda
+builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse
 
 end Lean

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

@@ -44,7 +44,7 @@ def propagateBetaEqs (lams : Array Expr) (f : Expr) (args : Array Expr) : GoalM
           gen := Nat.max gen (← getGeneration arg)
           h ← mkCongrFun h arg
         let eq ← mkEq lhs rhs
-        trace[grind.beta] "{eq}, using {lam}"
+        trace_goal[grind.beta] "{eq}, using {lam}"
         addNewFact h eq (gen+1)
 
 private def isPropagateBetaTarget (e : Expr) : GoalM Bool := do

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

@@ -86,15 +86,15 @@ def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBou
         -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
         -- and different locals are added in different branches.
         modify' fun s => { s with canon := s.canon.insert e c }
-        trace[grind.debugn.canon] "found {e} ===> {c}"
+        trace_goal[grind.debugn.canon] "found {e} ===> {c}"
         return c
       if useIsDefEqBounded then
         -- If `e` and `c` are not types, we use `isDefEqBounded`
         if (← isDefEqBounded e c parent) then
           modify' fun s => { s with canon := s.canon.insert e c }
-          trace[grind.debugn.canon] "found using `isDefEqBounded`: {e} ===> {c}"
+          trace_goal[grind.debugn.canon] "found using `isDefEqBounded`: {e} ===> {c}"
           return c
-  trace[grind.debug.canon] "({f}, {i}) ↦ {e}"
+  trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
   modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
   return e
 
@@ -173,7 +173,7 @@ where
           let mut args := args.toVector
           for h : i in [:args.size] do
             let arg := args[i]
-            trace[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+            trace_goal[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
             let arg' ← match (← shouldCanon pinfos i arg) with
             | .canonType  => canonType e f i arg
             | .canonInst  => canonInst e f i arg
@@ -197,7 +197,7 @@ end Canon
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
 def canon (e : Expr) : GoalM Expr := do
-  trace[grind.debug.canon] "{e}"
+  trace_goal[grind.debug.canon] "{e}"
   unsafe Canon.canonImpl e
 
 end Lean.Meta.Grind

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

@@ -85,6 +85,20 @@ def eraseCasesAttr (declName : Name) : CoreM Unit := do
   let s ← s.eraseDecl declName
   modifyEnv fun env => casesExt.modifyState env fun _ => s
 
+/--
+We say a free variable is "simple" to be processed by the cases tactic IF:
+- It is the latest and consequently there are no forward dependencies, OR
+- It is not a proposion.
+-/
+private def isSimpleFVar (e : Expr) : MetaM Bool := do
+  let .fvar fvarId := e | return false
+  let decl ← fvarId.getDecl
+  if decl.index == (← getLCtx).numIndices - 1 then
+    -- It is the latest free variable, so there are no forward dependencies
+    return true
+  else
+    -- It is pointless to add an auxiliary equality if `e`s type is a proposition
+    isProp decl.type
 
 /--
 The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users.
@@ -132,12 +146,17 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
     let s ← generalizeIndices' mvarId e
     s.mvarId.withContext do
       k s.mvarId s.fvarId s.indicesFVarIds
-  else if let .fvar fvarId := e then
-    k mvarId fvarId #[]
+  else if (← isSimpleFVar e) then
+    -- We don't need to revert anything.
+    k mvarId e.fvarId! #[]
   else
-    let mvarId ← mvarId.assert (← mkFreshUserName `x) type e
+    let mvarId ← if (← isProof e) then
+      mvarId.assert (← mkFreshUserName `x) type e
+    else
+      mvarId.assertExt (← mkFreshUserName `x) type e
     let (fvarId, mvarId) ← mvarId.intro1
     mvarId.withContext do k mvarId fvarId #[]
+
 where
   throwInductiveExpected {α} (type : Expr) : MetaM α := do
     throwTacticEx `grind.cases mvarId m!"(non-recursive) inductive type expected at {e}{indentExpr type}"

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

@@ -116,15 +116,15 @@ the lambda expressions in `lams`.
 def propagateBeta (lams : Array Expr) (fns : Array Expr) : GoalM Unit := do
   if lams.isEmpty then return ()
   let lamRoot ← getRoot lams.back!
-  trace[grind.debug.beta] "fns: {fns}, lams: {lams}"
+  trace_goal[grind.debug.beta] "fns: {fns}, lams: {lams}"
   for fn in fns do
-    trace[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).toArray}"
+    trace_goal[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).toArray}"
     for parent in (← getParents fn) do
       let mut args := #[]
       let mut curr := parent
-      trace[grind.debug.beta] "parent: {parent}"
+      trace_goal[grind.debug.beta] "parent: {parent}"
       repeat
-        trace[grind.debug.beta] "curr: {curr}"
+        trace_goal[grind.debug.beta] "curr: {curr}"
         if (← isEqv curr lamRoot) then
           propagateBetaEqs lams curr args.reverse
         let .app f arg := curr

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

@@ -98,7 +98,7 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
   else if (← isEqTrue e) then
     if let some (e', h') ← eqResolution e then
-      trace[grind.eqResolution] "{e}, {e'}"
+      trace_goal[grind.eqResolution] "{e}, {e'}"
       let h := mkOfEqTrueCore e (← mkEqTrueProof e)
       let h' := mkApp h' h
       addNewFact h' e' (← getGeneration e)

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

@@ -90,7 +90,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       else if (← getConfig).splitIndPred then
         addSplitCandidate e
   | .fvar .. =>
-    let .const declName _ := (← inferType e).getAppFn | return ()
+    let .const declName _ := (← whnfD (← inferType e)).getAppFn | return ()
     if (← get).casesTypes.isSplit declName then
       addSplitCandidate e
   | _ => pure ()
@@ -132,8 +132,8 @@ private def internalizeMatchCond (matchCond : Expr) (generation : Nat) : GoalM U
   lhss.forM fun lhs => do internalize lhs generation; registerParent matchCond lhs
   propagateUp matchCond
   internalize e' generation
-  trace[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}"
-  trace[grind.debug.matchCond.lambda] "auxiliary application{indentExpr e'}"
+  trace_goal[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}"
+  trace_goal[grind.debug.matchCond.lambda] "auxiliary application{indentExpr e'}"
   pushEq matchCond e' (← mkEqRefl matchCond)
 
 def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
@@ -191,7 +191,11 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
   match e with
   | .bvar .. => unreachable!
   | .sort .. => return ()
-  | .fvar .. | .letE .. | .lam .. => mkENode' e generation
+  | .fvar .. =>
+    mkENode' e generation
+    checkAndAddSplitCandidate e
+  | .letE .. | .lam .. =>
+    mkENode' e generation
   | .forallE _ d b _ =>
     mkENode' e generation
     if (← isProp d <&&> isProp e) then

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

@@ -267,7 +267,7 @@ private partial def isStatisfied (e : Expr) : GoalM Bool := do
   repeat
     let .forallE _ d b _ := e | break
     if (← isMatchCondFalseHyp d) then
-      trace[grind.debug.matchCond] "satifised{indentExpr e}\nthe following equality is false{indentExpr d}"
+      trace_goal[grind.debug.matchCond] "satifised{indentExpr e}\nthe following equality is false{indentExpr d}"
       return true
     e := b
   return false
@@ -279,13 +279,13 @@ private partial def mkMatchCondProof? (e : Expr) : GoalM (Option Expr) := do
     for x in xs do
       let type ← inferType x
       if (← isMatchCondFalseHyp type) then
-        trace[grind.debug.matchCond] ">>> {type}"
+        trace_goal[grind.debug.matchCond] ">>> {type}"
         let some h ← go? x | pure ()
         return some (← mkLambdaFVars xs h)
     return none
 where
   go? (h : Expr) : GoalM (Option Expr) := do
-    trace[grind.debug.matchCond] "go?: {← inferType h}"
+    trace_goal[grind.debug.matchCond] "go?: {← inferType h}"
     let some (α?, lhs, rhs) := isEqHEq? (← inferType h)
       | return none
     let target ← (← get).mvarId.getType
@@ -318,13 +318,28 @@ where
     else
       return none
 
+def tryToProveFalse (e : Expr) : GoalM Unit := do
+  trace_goal[grind.debug.matchCond.proveFalse] "{e}"
+  -- TODO
+  return ()
+
 /-- Propagates `MatchCond` upwards -/
-builtin_grind_propagator propagateMatchCond ↑Grind.MatchCond := fun e => do
-  trace[grind.debug.matchCond] "visiting{indentExpr e}"
-  if !(← isStatisfied e) then return ()
-  let some h ← mkMatchCondProof? e
-     | reportIssue m!"failed to construct proof for{indentExpr e}"; return ()
-  trace[grind.debug.matchCond] "{← inferType h}"
-  pushEqTrue e <| mkEqTrueCore e h
+builtin_grind_propagator propagateMatchCondUp ↑Grind.MatchCond := fun e => do
+  trace_goal[grind.debug.matchCond] "visiting{indentExpr e}"
+  if (← isEqTrue e) then
+    unless (← isStatisfied e) do
+      tryToProveFalse e
+  else
+    if !(← isStatisfied e) then return ()
+    let some h ← mkMatchCondProof? e
+       | reportIssue m!"failed to construct proof for{indentExpr e}"; return ()
+    trace_goal[grind.debug.matchCond] "{← inferType h}"
+    pushEqTrue e <| mkEqTrueCore e h
+
+/-- Propagates `MatchCond` downwards -/
+builtin_grind_propagator propagateMatchCondDown ↓Grind.MatchCond := fun e => do
+  if (← isEqTrue e) then
+    unless (← isStatisfied e) do
+      tryToProveFalse e
 
 end Lean.Meta.Grind

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

@@ -38,7 +38,7 @@ def simp (e : Expr) : GoalM Simp.Result := do
   let e' ← eraseSimpMatchDiscrsOnly e'
   let e' ← canon e'
   let e' ← shareCommon e'
-  trace[grind.simp] "{e}\n===>\n{e'}"
+  trace_goal[grind.simp] "{e}\n===>\n{e'}"
   return { r with expr := e' }
 
 end Lean.Meta.Grind

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

@@ -91,22 +91,25 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
   | dite _ c _ _ _ => checkIteCondStatus c
   | _ =>
     if (← isResolvedCaseSplit e) then
-      trace[grind.debug.split] "split resolved: {e}"
+      trace_goal[grind.debug.split] "split resolved: {e}"
       return .resolved
     if (← isCongrToPrevSplit e) then
       return .resolved
     if let some info := isMatcherAppCore? (← getEnv) e then
       return .ready info.numAlts
-    let .const declName .. := e.getAppFn | unreachable!
-    if let some info ← isInductivePredicate? declName then
-      if (← isEqTrue e) then
-        return .ready info.ctors.length info.isRec
+    if let .const declName .. := e.getAppFn then
+      if let some info ← isInductivePredicate? declName then
+        if (← isEqTrue e) then
+          return .ready info.ctors.length info.isRec
     if e.isFVar then
       let type ← whnfD (← inferType e)
+      trace[Meta.debug] "1. {e}"
       let report : GoalM Unit := do
         reportIssue "cannot perform case-split on {e}, unexpected type{indentExpr type}"
       let .const declName _ := type.getAppFn | report; return .resolved
+      trace[Meta.debug] "2. {e}"
       let .inductInfo info ← getConstInfo declName | report; return .resolved
+      trace[Meta.debug] "3. {e}"
       return .ready info.ctors.length info.isRec
     return .notReady
 
@@ -162,7 +165,11 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
     else
       return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
-  | _ => return mkOfEqTrueCore c (← mkEqTrueProof c)
+  | _ =>
+    if (← isEqTrue c) then
+      return mkOfEqTrueCore c (← mkEqTrueProof c)
+    else
+      return c
 
 /-- Introduces new hypotheses in each goal. -/
 private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do

tests/lean/run/grind_split_data.lean

@@ -0,0 +1,13 @@
+inductive C where
+  | a | b | c
+
+def f : C → Nat
+  | .a => 2
+  | .b => 3
+  | .c => 4
+
+example : f .a > 1 := by
+  grind [f]
+
+example : f x > 1 := by
+  grind [f, C]