test: for grind ite-issue

This PR fixes an issue in the `grind` tactic when case splitting on
if-then-else expressions.

It adds a new marker gadget that prevents `grind` for re-normalizing the condition `c` of an if-then-else
expression. Without this marker, the negated condition `¬c` might be rewritten into
an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`.
As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b`
in the `¬c` branch.

src/Init/Grind/Util.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
+import Init.Classical
 
 namespace Lean.Grind
 
@@ -77,5 +78,23 @@ def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
   | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
   | _ => throw ()
 
+/--
+A marker to indicate that a proposition has already been normalized and should not
+be processed again.
+
+This prevents issues when case-splitting on the condition `c` of an if-then-else
+expression. Without this marker, the negated condition `¬c` might be rewritten into
+an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`.
+As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b`
+in the `¬c` branch.
+-/
+def alreadyNorm (p : Prop) : Prop := p
+
+/--
+`Classical.em` variant where disjuncts are marked with `alreadyNorm` gadget.
+See comment at `alreadyNorm`
+-/
+theorem em (p : Prop) : alreadyNorm p ∨ alreadyNorm (¬ p) :=
+  Classical.em p
 
 end Lean.Grind

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

@@ -23,6 +23,14 @@ private inductive IntroResult where
   | newLocal (fvarId : FVarId) (goal : Goal)
   deriving Inhabited
 
+/--
+Returns `true` if `e` is marked with the `alreadyNorm` gadget.
+See `alreadyNorm` documentation for additional details
+-/
+private def isAlreadyNorm? (e : Expr) : Option Expr :=
+  let_expr Lean.Grind.alreadyNorm c := e | none
+  some c
+
 /--
 Similar to `Grind.preprocess`, but does not simplify `e` if
 `isMatchCondCandidate` (aka `Simp.isEqnThmHypothesis`) is `true`.
@@ -32,12 +40,14 @@ We added this feature because it may be coming from external sources
 private def preprocessHypothesis (e : Expr) : GoalM Simp.Result := do
   if isMatchCondCandidate e then
     preprocess (markAsPreMatchCond e)
+  else if let some c := isAlreadyNorm? e then
+    let c ← shareCommon (← canon c)
+    return { expr := c }
   else
     preprocess e
 
 /--
 Helper function for `mkCleanName`.
-Creates a base name for creating a clean name for `name`.
 It ensures base name is a simple `Name` and does not have a `_<idx>` suffix
 -/
 private def mkBaseName (name : Name) (type : Expr) : MetaM Name := do

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

@@ -151,12 +151,15 @@ where
       else
         go cs c? (c::cs')
 
+private def mkGrindEM (c : Expr) :=
+  mkApp (mkConst ``Lean.Grind.em) c
+
 /-- Constructs a major premise for the `cases` tactic used by `grind`. -/
 private def mkCasesMajor (c : Expr) : GoalM Expr := do
   match_expr c with
   | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
-  | ite _ c _ _ _ => return mkEM c
-  | dite _ c _ _ _ => return mkEM c
+  | ite _ c _ _ _ => return mkGrindEM c
+  | dite _ c _ _ _ => return mkGrindEM c
   | Eq _ a b =>
     if (← isEqTrue c) then
       return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)

tests/lean/run/grind_ite_split_issue.lean

@@ -0,0 +1,30 @@
+set_option grind.warning false
+
+attribute [grind =] Int.min_def Int.max_def
+
+example (a b : Int) : min a b = 10 → a ≥ 10 := by
+  grind
+
+example (a b : Int) : min a b ≤ a := by
+  grind
+
+example (a b : Int) : min a b ≤ b := by
+  grind
+
+example (a b : Int) : min a b ≤ min b a := by
+  grind
+
+example (a b : Int) : max a (min a b) ≥ a := by
+  grind
+
+example (a b : Int) : max a (min a b) ≥ min b a := by
+  grind
+
+example (a b : Int) : max a (max a b) ≥ b := by
+  grind
+
+example (a b : Int) : max a (max a b) ≥ a := by
+  grind
+
+example (a : Int) : max a a = a := by
+  grind