chore: remove examples that are already working

src/Init/Grind/Tactics.lean

@@ -59,6 +59,11 @@ structure Config where
   If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
   Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
   splitIndPred : Bool := false
+  /--
+  If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
+  it the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
+  -/
+  splitImp : Bool := false
   /-- By default, `grind` halts as soon as it encounters a sub-goal where no further progress can be made. -/
   failures : Nat := 1
   /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -13,6 +13,10 @@ namespace Lean.Meta.Grind.Arith
 def isNatType (e : Expr) : Bool :=
   e.isConstOf ``Nat
 
+/-- Returns `true` if `e` is of the form `Int` -/
+def isIntType (e : Expr) : Bool :=
+  e.isConstOf ``Int
+
 /-- Returns `true` if `e` is of the form `@instHAdd Nat instAddNat` -/
 def isInstAddNat (e : Expr) : Bool :=
   let_expr instHAdd a b := e | false
@@ -49,5 +53,15 @@ def isNatNum? (e : Expr) : Option Nat := Id.run do
   let .lit (.natVal k) := k | none
   some k
 
+def isSupportedType (e : Expr) : Bool :=
+  isNatType e || isIntType e
+
+partial def isRelevantPred (e : Expr) : Bool :=
+  match_expr e with
+  | Not p => isRelevantPred p
+  | LE.le α _ _ _ => isSupportedType α
+  | Eq α _ _ => isSupportedType α
+  | Dvd.dvd α _ _ _ => isSupportedType α
+  | _ => false
 
 end Lean.Meta.Grind.Arith

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

@@ -94,6 +94,9 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
     let .const declName _ := (← whnfD (← inferType e)).getAppFn | return ()
     if (← get).split.casesTypes.isSplit declName then
       addSplitCandidate e
+  | .forallE _ d _ _ =>
+    if Arith.isRelevantPred d || (← getConfig).splitImp then
+      addSplitCandidate e
   | _ => pure ()
 
 /--
@@ -237,6 +240,7 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
         internalizeImpl b generation e
         registerParent e b
       propagateUp e
+      checkAndAddSplitCandidate e
   | .lit .. =>
     mkENode e generation
   | .const declName _ =>

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

@@ -15,7 +15,7 @@ inductive CaseSplitStatus where
   | resolved
   | notReady
   | ready (numCases : Nat) (isRec := false)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Repr
 
 /-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/
 private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do
@@ -82,6 +82,17 @@ private def isCongrToPrevSplit (c : Expr) : GoalM Bool := do
     else
       return isCongruent (← get).enodes c c'
 
+private def checkForallStatus (e : Expr) : GoalM CaseSplitStatus := do
+  if (← isEqTrue e) then
+    let .forallE _ p _ _ := e | return .resolved
+    if (← isEqTrue p <||> isEqFalse p) then
+      return .resolved
+    return .ready 2
+  else if (← isEqFalse e) then
+    return .resolved
+  else
+    return .notReady
+
 private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
   match_expr e with
   | Or a b => checkDisjunctStatus e a b
@@ -97,6 +108,10 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
     if (← isResolvedCaseSplit e) then
       trace_goal[grind.debug.split] "split resolved: {e}"
       return .resolved
+    if e.isForall then
+      let s ← checkForallStatus e
+      trace_goal[grind.debug.split] "{e}, status: {repr s}"
+      return s
     if (← isCongrToPrevSplit e) then
       return .resolved
     if let some info := isMatcherAppCore? (← getEnv) e then
@@ -137,6 +152,7 @@ where
         modify fun s => { s with split.num := numSplits, ematch.num := 0 }
       return c?
     | c::cs =>
+    trace_goal[grind.debug.split] "checking: {c}"
     match (← checkCaseSplitStatus c) with
     | .notReady => go cs c? (c::cs')
     | .resolved => go cs c? cs'
@@ -174,7 +190,9 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       -- model-based theory combination split
       return mkGrindEM c
   | _ =>
-    if (← isEqTrue c) then
+    if let .forallE _ p _ _ := c then
+      return mkGrindEM p
+    else if (← isEqTrue c) then
       return mkOfEqTrueCore c (← mkEqTrueProof c)
     else
       return c

tests/lean/grind/list_problems.lean

@@ -1,27 +1,5 @@
 reset_grind_attrs%
 
-attribute [grind] List.length_set
-attribute [grind →] List.eq_nil_of_length_eq_zero
-
-open List in
-example {as : List α} {i : Nat} (h : i < as.length) :
-    as.set i as[i] = as := by
-  apply ext_getElem
-  · sorry
-  · -- works:
-    grind [getElem_set]
-
-attribute [grind] List.getElem_set
-
-open List in
-example {as : List α} {i : Nat} (h : i < as.length) :
-    as.set i as[i] = as := by
-  apply ext_getElem
-  · sorry
-  · -- fails:
-    grind
-
----
 reset_grind_attrs%
 
 theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by

tests/lean/grind/model_conjectures.lean

@@ -1,36 +0,0 @@
-attribute [grind] Vector.getElem_swap_of_ne
-
-/- This fails, but after obtaining the cutsat model:
-```
-  [cutsat] Assignment satisfying linear contraints ▼
-    [assign] i := 2
-    [assign] n := 3
-    [assign] j := 1
-    [assign] k := 0
-```
-it would be reasonable to look at the asserted fact
-```
-¬k = i → ¬k = j → (as.swap i j ⋯ ⋯)[k] = as[k]
-```
-and conjecture that `¬k = i` is true, and derive a proof for this from cutsat.
--/
-example (hi : i < n) (hj : j < i) (hk : k < j) (as : Vector α n) (p : α → Prop) (h : p as[k]) :
-    p (as.swap i j)[k] := by
-  grind
-
-/- Similarly here, we fail with the asserted facts (among others):
-```
-    [prop] i ≤ j
-    [prop] ¬p i
-    [prop] i + 1 ≤ j → p i
-    [prop] ¬j = i
-```
-and the cutsat model:
-```
-  [cutsat] Assignment satisfying linear contraints ▼
-    [assign] j := 1
-    [assign] i := 0
-```
-At this point it would be reasonable to conjecture that `i + 1 ≤ j`.
--/
-example (p : Nat → Prop) (h : p j) (h' : ∀ i, i < j → p i) : ∀ i, i < j + 1 → p i := by grind

tests/lean/run/grind_split_arith_imp.lean

@@ -0,0 +1,9 @@
+reset_grind_attrs%
+set_option grind.warning false
+attribute [grind] Vector.getElem_swap_of_ne
+
+example (hi : i < n) (hj : j < i) (hk : k < j) (as : Vector α n) (p : α → Prop) (h : p as[k]) :
+    p (as.swap i j)[k] := by
+  grind
+
+example (p : Nat → Prop) (h : p j) (h' : ∀ i, i < j → p i) : ∀ i, i < j + 1 → p i := by grind

tests/lean/run/grind_t1.lean

@@ -424,3 +424,6 @@ example [BEq α] [LawfulBEq α] (a b : α) : a ≠ b → foo a b = 0 := by
 @[simp] theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
     (l ++ [a])[i]'w = a := by
   subst h; grind [List.getElem_append_left, List.getElem_append_right]
+
+example (p q : Prop) : (p → q) → (¬ p → q) → (p → ¬ q) → (¬p → ¬q) → False := by
+  grind (splitImp := true)