test: another test

Only cases with one minor premise are considered

src/Init/Grind/Lemmas.lean

@@ -165,4 +165,9 @@ theorem of_decide_eq_false {p : Prop} {_ : Decidable p} : decide p = false → p
 theorem decide_eq_true {p : Prop} {_ : Decidable p} : p = True → decide p = true := by simp
 theorem decide_eq_false {p : Prop} {_ : Decidable p} : p = False → decide p = false := by simp
 
+/-! Lookahead -/
+
+theorem of_lookahead (p : Prop) (h : (¬ p) → False) : p = True := by
+  simp at h; simp [h]
+
 end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -75,6 +75,8 @@ structure Config where
   on equalities between lambda expressions.
   -/
   funext : Bool := true
+  /-- TODO -/
+  lookahead : Bool := true
   /-- If `verbose` is `false`, additional diagnostics information is not collected. -/
   verbose : Bool := true
   /-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/

src/Lean/Meta/Tactic/Grind.lean

@@ -30,6 +30,7 @@ import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.MBTC
+import Lean.Meta.Tactic.Grind.Lookahead
 
 namespace Lean
 
@@ -54,6 +55,10 @@ builtin_initialize registerTraceClass `grind.beta
 builtin_initialize registerTraceClass `grind.mbtc
 builtin_initialize registerTraceClass `grind.ext
 builtin_initialize registerTraceClass `grind.ext.candidate
+builtin_initialize registerTraceClass `grind.lookahead
+builtin_initialize registerTraceClass `grind.lookahead.add (inherited := true)
+builtin_initialize registerTraceClass `grind.lookahead.try (inherited := true)
+builtin_initialize registerTraceClass `grind.lookahead.assert (inherited := true)
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug

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

@@ -90,8 +90,13 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
     if (← get).split.casesTypes.isSplit declName then
       addSplitCandidate e
   | .forallE _ d _ _ =>
-    if Arith.isRelevantPred d || (← getConfig).splitImp then
+    if (← getConfig).splitImp then
       addSplitCandidate e
+    else if Arith.isRelevantPred d then
+      if (← getConfig).lookahead then
+        addLookaheadCandidate (.imp e)
+      else
+        addSplitCandidate e
   | _ => pure ()
 
 /--
@@ -167,7 +172,7 @@ private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Un
     modify fun s => { s with ematch.thmMap := thmMap }
     let appMap := (← get).appMap
     for thm in thms do
-      trace[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`"
+      trace_goal[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`"
       unless (← get).ematch.thmMap.isErased thm.origin do
         let symbols := thm.symbols.filter fun sym => !appMap.contains sym
         let thm := { thm with symbols }
@@ -208,13 +213,13 @@ private def extParentsToIgnore (declName : Name) : Bool :=
   || declName == ``Exists || declName == ``Subtype
 
 /--
-Given a term `e` that occurs as the argument at position `i` of an `f`-application `parent?`,
-we consider `e` as a candidate for case-splitting. For every other argument `e'` that also appears
-at position `i` in an `f`-application and has the same type as `e`, we add the case-split candidate `e = e'`.
+Given a term `arg` that occurs as the argument at position `i` of an `f`-application `parent?`,
+we consider `arg` as a candidate for case-splitting. For every other argument `arg'` that also appears
+at position `i` in an `f`-application and has the same type as `e`, we add the case-split candidate `arg = arg'`.
 
 When performing the case split, we consider the following two cases:
-- `e = e'`, which may introduce a new congruence between the corresponding `f`-applications.
-- `¬(e = e')`, which may trigger extensionality theorems for the type of `e`.
+- `arg = arg'`, which may introduce a new congruence between the corresponding `f`-applications.
+- `¬(arg = arg')`, which may trigger extensionality theorems for the type of `arg`.
 
 This feature enables `grind` to solve examples such as:
 ```lean
@@ -222,13 +227,13 @@ example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x =>
   grind
 ```
 -/
-private def addSplitCandidatesForExt (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
+private def addSplitCandidatesForExt (arg : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
   let some parent := parent? | return ()
   unless parent.isApp do return ()
   let f := parent.getAppFn
   if let .const declName _ := f then
     if extParentsToIgnore declName then return ()
-  let type ← inferType e
+  let type ← inferType arg
   -- Remark: we currently do not perform function extensionality on functions that produce a type that is not a proposition.
   -- We may add an option to enable that in the future.
   let u? ← typeFormerTypeLevel type
@@ -238,28 +243,31 @@ private def addSplitCandidatesForExt (e : Expr) (generation : Nat) (parent? : Op
   repeat
     if !it.isApp then return ()
     i := i - 1
-    let arg := it.appArg!
-    if isSameExpr arg e then
-      found f i type
+    if isSameExpr arg it.appArg! then
+      found f i type parent
     it := it.appFn!
 where
-  found (f : Expr) (i : Nat) (type : Expr) : GoalM Unit := do
-    trace[grind.debug.ext] "{f}, {i}, {e}"
-    let others := (← get).termsAt.find? (f, i) |>.getD []
-    for (e', type') in others do
-      if (← withDefault <| isDefEq type type') then
-        let eq := mkApp3 (mkConst ``Eq [← getLevel type]) type e e'
+  found (f : Expr) (i : Nat) (type : Expr) (parent : Expr) : GoalM Unit := do
+    trace_goal[grind.debug.ext] "{f}, {i}, {arg}"
+    let others := (← get).split.argsAt.find? (f, i) |>.getD []
+    for other in others do
+      if (← withDefault <| isDefEq type other.type) then
+        let eq := mkApp3 (mkConst ``Eq [← getLevel type]) type arg other.arg
         let eq ← shareCommon eq
         internalize eq generation
         trace_goal[grind.ext.candidate] "{eq}"
+        -- We do not use lookahead here because it is too incomplete.
+        -- if (← getConfig).lookahead then
+        --   addLookaheadCandidate (.arg other.app parent i eq)
+        -- else
         addSplitCandidate eq
-    modify fun s => { s with termsAt := s.termsAt.insert (f, i) ((e, type) :: others) }
+    modify fun s => { s with split.argsAt := s.split.argsAt.insert (f, i) ({ arg, type, app := parent } :: others) }
     return ()
 
 /-- Applies `addSplitCandidatesForExt` if `funext` is enabled. -/
-private def addSplitCandidatesForFunext (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
+private def addSplitCandidatesForFunext (arg : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
   unless (← getConfig).funext do return ()
-  addSplitCandidatesForExt e generation parent?
+  addSplitCandidatesForExt arg generation parent?
 
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do

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

@@ -178,6 +178,12 @@ private def isEagerCasesCandidate (goal : Goal) (type : Expr) : Bool := Id.run d
   let .const declName _ := type.getAppFn | return false
   return goal.split.casesTypes.isEagerSplit declName
 
+/-- Returns `true` if `type` is an inductive type with at most one constructor. -/
+private def isCheapInductive (type : Expr) : CoreM Bool := do
+  let .const declName _ := type.getAppFn | return false
+  let .inductInfo info ← getConstInfo declName | return false
+  return info.numCtors <= 1
+
 private def applyCases? (goal : Goal) (fvarId : FVarId) : GrindM (Option (List Goal)) := goal.mvarId.withContext do
   /-
   Remark: we used to use `whnfD`. This was a mistake, we don't want to unfold user-defined abstractions.
@@ -185,6 +191,9 @@ private def applyCases? (goal : Goal) (fvarId : FVarId) : GrindM (Option (List G
   -/
   let type ← whnf (← fvarId.getType)
   if isEagerCasesCandidate goal type then
+    if (← cheapCasesOnly) then
+      unless (← isCheapInductive type) do
+        return none
     if let .const declName _ := type.getAppFn then
       saveCases declName true
     let mvarIds ← cases goal.mvarId (mkFVar fvarId)
@@ -205,7 +214,7 @@ private def exfalsoIfNotProp (goal : Goal) : MetaM Goal := goal.mvarId.withConte
     return { goal with mvarId := (← goal.mvarId.exfalso) }
 
 /-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
-partial def intros  (generation : Nat) : GrindTactic' := fun goal => do
+partial def intros (generation : Nat) : GrindTactic' := fun goal => do
   let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
     if goal.inconsistent then
       return ()

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

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.Arith
+import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.EMatch
+
+namespace Lean.Meta.Grind
+
+inductive LookaheadStatus where
+  | resolved
+  | notReady
+  | ready
+  deriving Inhabited, BEq, Repr
+
+private def checkLookaheadStatus (info : LookaheadInfo) : GoalM LookaheadStatus := do
+  match info with
+  | .imp e =>
+    unless (← isEqTrue e) do return .notReady
+    let .forallE _ d b _ := e | unreachable!
+    if (← isEqTrue d <||> isEqFalse d) then return .resolved
+    unless b.hasLooseBVars do
+      if (← isEqTrue b <||> isEqFalse b) then return .resolved
+    return .ready
+  | .arg a b _ eq =>
+    if (← isEqTrue eq <||> isEqFalse eq) then return .resolved
+    let is := (← get).split.lookaheadArgPos[(a, b)]? |>.getD []
+    let mut j := a.getAppNumArgs
+    let mut it_a := a
+    let mut it_b := b
+    repeat
+      unless it_a.isApp && it_b.isApp do return .ready
+      j := j - 1
+      if j ∉ is then
+        let arg_a := it_a.appArg!
+        let arg_b := it_b.appArg!
+        unless (← isEqv arg_a arg_b) do
+          return .notReady
+      it_a := it_a.appFn!
+      it_b := it_b.appFn!
+    return .ready
+
+private partial def solve (generation : Nat) (goal : Goal) : GrindM Bool := do
+  cont (← intros generation goal)
+where
+  cont (goals : List Goal) : GrindM Bool := do
+    match goals with
+    | [] => return true
+    | [goal] => loop goal
+    | _ => throwError "`grind` lookahead internal error, unexpected number of goals"
+
+  loop (goal : Goal) : GrindM Bool := withIncRecDepth do
+    if goal.inconsistent then
+      return true
+    else if let some goals ← assertNext goal then
+      cont goals
+    else if let some goals ← Arith.check goal then
+      cont goals
+    else if let some goals ← splitNext goal then
+      cont goals
+    else if let some goals ← ematchAndAssert goal then
+      cont goals
+    else
+      return false
+
+private def tryLookahead (e : Expr) : GoalM Bool := do
+  -- TODO: if `e` is an arithmetic expression, we can avoid creating an auxiliary goal.
+  -- We can assert it directly to the arithmetic module.
+  -- Remark: We can simplify this code because the lookahead only really worked for arithmetic.
+  trace_goal[grind.lookahead.try] "{e}"
+  let proof? ← withoutModifyingState do
+    let goal ← get
+    let tag ← goal.mvarId.getTag
+    let target ← mkArrow (mkNot e) (← getFalseExpr)
+    let mvar ← mkFreshExprMVar target .syntheticOpaque tag
+    let gen ← getGeneration e
+    if (← solve gen { goal with mvarId := mvar.mvarId! }) then
+      return some (← instantiateMVars mvar)
+    else
+      return none
+  if let some proof := proof? then
+    trace[grind.lookahead.assert] "{e}"
+    pushEqTrue e <| mkApp2 (mkConst ``Grind.of_lookahead) e proof
+    processNewFacts
+    return true
+  else
+    return false
+
+private def withLookaheadConfig (x : GrindM α) : GrindM α := do
+  withTheReader Grind.Context
+    (fun ctx => { ctx with config.qlia := true, cheapCases := true })
+    x
+
+def lookahead : GrindTactic := fun goal => do
+  unless (← getConfig).lookahead do
+    return none
+  if goal.split.lookaheads.isEmpty then
+    return none
+  withLookaheadConfig do
+  let (progress, goal) ← GoalM.run goal do
+    let mut postponed := []
+    let mut progress := false
+    let infos := (← get).split.lookaheads
+    modify fun s => { s with split.lookaheads := [] }
+    for info in infos do
+      if (← isInconsistent) then
+        return true
+      match (← checkLookaheadStatus info) with
+      | .resolved => progress := true
+      | .notReady => postponed := info :: postponed
+      | .ready =>
+        if (← tryLookahead info.getExpr) then
+          progress := true
+        else
+          postponed := info :: postponed
+    if progress then
+      modify fun s => { s with
+        split.lookaheads := s.split.lookaheads ++ postponed.reverse
+      }
+      return true
+    else
+      return false
+  if progress then
+    return some [goal]
+  else
+    return none
+
+end Lean.Meta.Grind

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

@@ -9,18 +9,6 @@ import Lean.Meta.Tactic.Grind.Simp
 
 namespace Lean.Meta.Grind
 
-/--
-Helper function for executing `x` with a fresh `newFacts` and without modifying
-the goal state.
- -/
-private def withoutModifyingState (x : GoalM α) : GoalM α := do
-  let saved ← get
-  modify fun goal => { goal with newFacts := {} }
-  try
-    x
-  finally
-    set saved
-
 /--
 If `e` has not been internalized yet, instantiate metavariables, unfold reducible, canonicalize,
 and internalize the result.

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

@@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Grind.Combinators
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Arith
+import Lean.Meta.Tactic.Grind.Lookahead
 
 namespace Lean.Meta.Grind
 
@@ -62,6 +63,8 @@ def trySplit : Goal → M Bool := applyTac splitNext
 
 def tryArith : Goal → M Bool := applyTac Arith.check
 
+def tryLookahead : Goal → M Bool := applyTac lookahead
+
 def tryMBTC : Goal → M Bool := applyTac Arith.Cutsat.mbtcTac
 
 def maxNumFailuresReached : M Bool := do
@@ -81,6 +84,8 @@ partial def main (fallback : Fallback) : M Unit := do
       continue
     if (← tryEmatch goal) then
       continue
+    if (← tryLookahead goal) then
+      continue
     if (← trySplit goal) then
       continue
     if (← tryMBTC goal) then

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

@@ -161,7 +161,9 @@ where
     | .notReady => go cs c? (c::cs')
     | .resolved => go cs c? cs'
     | .ready numCases isRec =>
-    match c? with
+    if (← cheapCasesOnly) && numCases > 1 then
+      go cs c? (c::cs')
+    else match c? with
     | .none => go cs (.some c numCases isRec) cs'
     | .some c' numCases' _ =>
      let isBetter : GoalM Bool := do

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

@@ -58,6 +58,15 @@ structure Context where
   simprocs     : Array Simp.Simprocs
   mainDeclName : Name
   config       : Grind.Config
+  /--
+  If `cheapCases` is `true`, `grind` only applies `cases` to types that contain
+  at most one minor premise.
+  Recall that `grind` applies `cases` when introducing types tagged with `[grind cases eager]`,
+  and at `Split.lean`
+  Remark: We add this option to implement the `lookahead` feature, we don't want to create several subgoals
+  when performing lookahead.
+  -/
+  cheapCases : Bool := false
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -164,6 +173,9 @@ def getNatZeroExpr : GrindM Expr := do
 def getMainDeclName : GrindM Name :=
   return (← readThe Context).mainDeclName
 
+def cheapCasesOnly : GrindM Bool :=
+  return (← readThe Context).cheapCases
+
 def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
   if (← getConfig).trace then
     modify fun s => { s with trace.thms := s.trace.thms.insert { origin := thm.origin, kind := thm.kind } }
@@ -472,24 +484,73 @@ structure EMatch.State where
   matchEqNames : PHashSet Name := {}
   deriving Inhabited
 
+/--
+Lookahead case-split information. They are cheaper than regular case-splits.
+They are created when `Grind.Config.lookahead` is `true`.
+The idea is the following: `grind` asserts `¬ p`, if a contradiction is detected
+it asserts `p`.
+-/
+inductive LookaheadInfo where
+  | /--
+    Given an implication `e`, use lookahead to check whether the antecedent is
+    implied to be `True`. The lookahead is marked as resolved if the consequent is already
+    known to be `True`.
+    -/
+    imp (e : Expr)
+  | /--
+    Given applications `a` and `b`, use lookahead to check whether the corresponding
+    `i`-th arguments are equal or not. The lookahead is only performed if all other
+    arguments are already known to be equal or are also tagged as lookahead.
+    `eq` is the equality between the two arguments
+    -/
+    arg (a b : Expr) (i : Nat) (eq : Expr)
+
+/-- Returns expression to perform a lookahead case-split. -/
+def LookaheadInfo.getExpr : LookaheadInfo → Expr
+  | .imp e => e.bindingDomain!
+  | .arg _ _ _ eq => eq
+
+/-- Argument `arg : type` of an application `app` -/
+structure Arg where
+  arg  : Expr
+  type : Expr
+  app  : Expr
+
 /-- Case splitting related fields for the `grind` goal. -/
 structure Split.State where
   /-- Inductive datatypes marked for case-splitting -/
-  casesTypes : CasesTypes := {}
+  casesTypes      : CasesTypes := {}
   /-- Case-split candidates. -/
-  candidates : List Expr := []
+  candidates      : List Expr := []
   /-- Number of splits performed to get to this goal. -/
-  num        : Nat := 0
+  num             : Nat := 0
   /-- Case-splits that have been inserted at `candidates` at some point. -/
-  added      : PHashSet ENodeKey := {}
+  added           : PHashSet ENodeKey := {}
   /-- Case-splits that have already been performed, or that do not have to be performed anymore. -/
-  resolved   : PHashSet ENodeKey := {}
+  resolved        : PHashSet ENodeKey := {}
   /--
   Sequence of cases steps that generated this goal. We only use this information for diagnostics.
   Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases`
   applications that generated only 1 subgoal.
   -/
-  trace      : List CaseTrace := []
+  trace           : List CaseTrace := []
+  /-- Lookahead "case-splits". -/
+  lookaheads      : List LookaheadInfo := []
+  /--
+  A mapping `(a, b) ↦ is` s.t. for each `LookaheadInfo.arg a b i eq`
+  in `lookaheads` we have `i ∈ is`.
+  We use this information to decide whether the lookahead is "ready"
+  to be tried or not.
+  -/
+  lookaheadArgPos : Std.HashMap (Expr × Expr) (List Nat) := {}
+  /--
+  Mapping from pairs `(f, i)` to a list of arguments.
+  Each argument occurs as the `i`-th of an `f`-application.
+  We use this information to add case-splits for
+  triggering extensionality theorems and model-based theory combination.
+  See `addSplitCandidatesForExt`.
+  -/
+  argsAt          : PHashMap (Expr × Nat) (List Arg) := {}
   deriving Inhabited
 
 /-- Clean name generator. -/
@@ -531,13 +592,6 @@ structure Goal where
   arith      : Arith.State := {}
   /-- State of the clean name generator. -/
   clean      : Clean.State := {}
-  /--
-  Mapping from pairs `(f, i)` to a list of `(e, type)`.
-  The meaning is: `e : type` is lambda expression that occurs at argument `i` of an `f`-application.
-  We use this information to add case-splits for triggering extensionality theorems.
-  See `addSplitCandidatesForExt`.
-  -/
-  termsAt    : PHashMap (Expr × Nat) (List (Expr × Expr)) := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -1214,4 +1268,30 @@ def synthesizeInstanceAndAssign (x type : Expr) : MetaM Bool := do
   let .some val ← trySynthInstance type | return false
   isDefEq x val
 
+/-- Add a new lookahead candidate. -/
+def addLookaheadCandidate (info : LookaheadInfo) : GoalM Unit := do
+  trace_goal[grind.lookahead.add] "{info.getExpr}"
+  match info with
+  | .imp .. =>
+    modify fun s => { s with split.lookaheads := info :: s.split.lookaheads }
+  | .arg a b i _ =>
+    let key := (a, b)
+    let is := (← get).split.lookaheadArgPos[key]? |>.getD []
+    modify fun s => { s with
+      split.lookaheads := info :: s.split.lookaheads
+      split.lookaheadArgPos := s.split.lookaheadArgPos.insert key (i :: is)
+    }
+
+/--
+Helper function for executing `x` with a fresh `newFacts` and without modifying
+the goal state.
+-/
+def withoutModifyingState (x : GoalM α) : GoalM α := do
+  let saved ← get
+  modify fun goal => { goal with newFacts := {} }
+  try
+    x
+  finally
+    set saved
+
 end Lean.Meta.Grind

tests/lean/run/grind_funext.lean

@@ -1,6 +1,13 @@
-example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
+
+set_option grind.warning false
+
+example (f : (Nat → Nat) → Nat → Nat → Nat) : a = b → f (fun x => a + x) 1 b = f (fun x => b + x) 1 a := by
   grind
 
 example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
   fail_if_success grind -funext
   sorry
+
+example (g : Nat → Nat → Nat) (f : (Nat → Nat) → Nat → (Nat → Nat) → Nat) :
+    a = b → f (fun x => a + x) 1 (fun x => g x a) = f (fun x => x + b) 1 (fun x => g x b) := by
+  grind

tests/lean/run/grind_lookahead.lean

@@ -0,0 +1,19 @@
+set_option grind.warning false
+reset_grind_attrs%
+
+attribute [grind] List.eq_nil_of_length_eq_zero
+
+example (as : List α) (h : as.length < 2) (h : as.length ≠ 1) (f : List α → Nat) :
+    f as = f [] := by
+  grind
+
+example (as : List α) (h : as.length < 2) (h : as.length ≠ 1) : as = [] := by
+  grind -lookahead
+
+example (as : List α) (h : as.length < 2) (h : as.length ≠ 1) : as = [] := by
+  grind (splits := 0)
+
+example (as : List α) (h : as.length < 2) (h : as.length ≠ 1) (f : List α → Nat)
+    : f as = f [] := by
+  fail_if_success grind (splits := 0) -lookahead -- Need lookahead or case-splits
+  sorry

tests/lean/run/grind_split_arith_imp.lean

@@ -4,7 +4,16 @@ 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
+  grind (splits := 0)
+
+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 -lookahead
+
+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
+  fail_if_success grind (splits := 0) -lookahead -- needs lookahead or case-splits
+  sorry
 
 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_trace.lean

@@ -35,7 +35,7 @@ example : 0 < (x :: t).length := by
 /--
 info: Try this: grind only [= Option.map_some, = Option.map_none, = List.getElem?_replicate, = List.getElem?_eq_some_iff, =
   List.getElem?_map, = List.getElem_replicate, = List.getElem?_eq_none, = List.length_replicate, →
-  List.getElem?_eq_getElem, cases Or]
+  List.getElem?_eq_getElem]
 -/
 #guard_msgs (info) in
 theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) := by