chore: move example

This test is easy for `grind`, we just need to annotate `Nat.min_def`.

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

@@ -114,4 +114,13 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
         -- (a → b) = True → b = False → a = False
         pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
 
+builtin_grind_propagator propagateExistsDown ↓Exists := fun e => do
+  if (← isEqFalse e) then
+    let_expr f@Exists α p := e | return ()
+    let u := f.constLevels!
+    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)
+
 end Lean.Meta.Grind

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

@@ -76,11 +76,12 @@ private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
 
 /-- Returns `true` is `c` is congruent to a case-split that was already performed. -/
 private def isCongrToPrevSplit (c : Expr) : GoalM Bool := do
+  unless c.isApp do return false
   (← get).split.resolved.foldM (init := false) fun flag { expr := c' } => do
     if flag then
       return true
     else
-      return isCongruent (← get).enodes c c'
+      return c'.isApp && isCongruent (← get).enodes c c'
 
 private def checkForallStatus (e : Expr) : GoalM CaseSplitStatus := do
   if (← isEqTrue e) then

tests/lean/grind/list_problems.lean

@@ -1,20 +1,5 @@
 reset_grind_attrs%
 
-reset_grind_attrs%
-
-theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
-  induction l
-  · sorry
-  · cases i
-    · -- Better support for implication and dependent implication.
-      -- We need inequality propagation (or case-splits)
-      grind
-    · -- Similarly
-      grind
-
----
-reset_grind_attrs%
-
 attribute [grind] List.getElem_append_left List.getElem_append_right
 attribute [grind] List.length_cons List.length_nil
 

tests/lean/run/grind_getElem.lean

@@ -0,0 +1,10 @@
+set_option grind.warning false
+reset_grind_attrs%
+
+attribute [grind]
+  List.length_cons List.length_nil
+  List.getElem_cons
+  List.getElem?_cons List.getElem?_nil
+
+theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
+  induction l generalizing i <;> grind

tests/lean/run/grind_min.lean

@@ -1,4 +1,7 @@
+set_option grind.warning false
+reset_grind_attrs%
+attribute [grind =] Nat.min_def -- This annotation should eventually be in the Std library
+
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
     (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by
-  -- grind -- fails
-  omega
+  grind