chore: give preference of tactics of the same kind

feat: `max` and `missing` flags

feat: add `try? -only`

chore: rename `grind` related tests

We view `try?` and `grind` as cousins

chore: fix test

doc: `grind` no cut

feat: generate all combinations

src/Init/Try.lean

@@ -19,6 +19,12 @@ structure Config where
   lib := true
   /-- If `targetOnly` is `true`, `try?` collects information using the goal target only. -/
   targetOnly := false
+  /-- Maximum number of suggestions. -/
+  max := 8
+  /-- If `missing` is `true`, allows the construction of partial solutions where some of the subgoals are `sorry`. -/
+  missing := false
+  /-- If `only` is `true`, generates solutions using `grind only` and `simp only`. -/
+  only := true
   deriving Inhabited
 
 end Lean.Try

src/Lean/Elab/Tactic/Try.lean

@@ -116,40 +116,6 @@ private def getKindsSolvedAll (tacss : Array (Array (TSyntax `tactic))) : Array
         r := r.push k
     return r
 
-private def peekOne (tac1 : TSyntax `tactic) (tacss2 : Array (Array (TSyntax `tactic))) : TacticM (TSyntax `tactic) := do
-  let mut tacs2 := #[]
-  for s in tacss2 do
-    if s.isEmpty then
-      tacs2 := tacs2.push (← `(tactic| · sorry))
-    else
-      tacs2 := tacs2.push (← `(tactic| · $(s[0]!):tactic))
-  `(tactic| · $tac1:tactic
-              $tacs2*)
-
-private def mkChainResult (tac1 : TSyntax `tactic) (tacss2 : Array (TSyntax `tactic)) : TacticM (TSyntax `tactic) := do
-  let tacss2 := tacss2.map getSuggestionsCore
-  if (← isTracingEnabledFor `try.debug) then
-    trace[try.debug] "mkChainResultCore tac1{indentD tac1}"
-    let mut i : Nat := 0
-    for tacs2 in tacss2 do
-      i := i + 1
-      trace[try.debug] "goal #{i} tactics"
-      for tac2 in tacs2 do
-        trace[try.debug] "  {tac2}"
-    trace[try.debug] "mkChainResult -----"
-  let mut acc := #[]
-  let solvedAll := getTacsSolvedAll tacss2
-  for tac2 in solvedAll do
-    acc := acc.push (← `(tactic| $tac1 <;> $tac2))
-  let tacss2 := eraseTacs tacss2 solvedAll
-  -- TODO: mixed cases
-  trace[try.debug] "kinds: {getKindsSolvedAll tacss2}"
-  if (!acc.isEmpty && tacss2.all fun s => !s.isEmpty)
-     -- We only include partial solutions if there are no other solutions.
-     || (acc.isEmpty && tacss2.any fun s => !s.isEmpty) then
-    acc := acc.push <| (← peekOne tac1 tacss2)
-  mkTrySuggestions acc
-
 private def evalSuggestAtomic (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do
   let goals ← getGoals
   evalTactic tac.raw
@@ -171,29 +137,6 @@ private def simpTraceToSimp (tac : TSyntax `tactic) : TacticM (TSyntax `tactic)
     `(tactic| simp $config:optConfig $[only%$only]? $[[$args,*]]? $(loc)?)
   | _ => throwUnsupportedSyntax
 
-private def evalSuggestGrindTrace (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do
-  match tac with
-  | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    let config ← elabGrindConfig configStx
-    let config := { config with trace := true, verbose := false }
-    let trace ← evalGrindCore tac config only params fallback?
-    let tac ← grindTraceToGrind tac
-    let tac' ← mkGrindOnly configStx fallback? trace
-    trace[try.debug] "`grind` succeeded"
-    mkTrySuggestions #[tac, tac']
-  | _ => throwUnsupportedSyntax
-
-private def evalSuggestSimpTrace (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := withMainContext do
-  match tac with
-  | `(tactic| simp? $_:optConfig $[only%$only]? $[[$args,*]]? $(loc)?) =>
-    let tac ← simpTraceToSimp tac
-    let { ctx, simprocs, .. } ← mkSimpContext tac (eraseLocal := false)
-    let stats ← simpLocation ctx (simprocs := simprocs) none <| (loc.map expandLocation).getD (.targets #[] true)
-    let tac' ← mkSimpCallStx tac stats.usedTheorems
-    trace[try.debug] "`simp` succeeded"
-    mkTrySuggestions #[tac, tac']
-  | _ => throwUnsupportedSyntax
-
 abbrev TacticResult (α : Type) := EStateM.Result Exception SavedState α
 
 structure Ctx where
@@ -226,6 +169,92 @@ def observing (x : M α) : M (TacticResult α) := do
       s.restore (restoreInfo := true)
       return .error ex sNew
 
+private def mkChainResult (tac1 : TSyntax `tactic) (tacss2 : Array (TSyntax `tactic)) : M (TSyntax `tactic) := do
+  let tacss2 := tacss2.map getSuggestionsCore
+  if (← isTracingEnabledFor `try.debug) then
+    trace[try.debug] "mkChainResultCore tac1{indentD tac1}"
+    let mut i : Nat := 0
+    for tacs2 in tacss2 do
+      i := i + 1
+      trace[try.debug] "goal #{i} tactics"
+      for tac2 in tacs2 do
+        trace[try.debug] "  {tac2}"
+    trace[try.debug] "mkChainResult -----"
+  let mut acc := #[]
+  let solvedAll := getTacsSolvedAll tacss2
+  -- Give preference to tactics that solved all subgoals
+  for tac2 in solvedAll do
+    acc := acc.push (← `(tactic| $tac1 <;> $tac2))
+  /-
+  We claim mixed solutions using tactics in `solvedAll` are suboptimal, and should not be considered
+  Example: if `grind` solved all subgoals, we should not propose a solution such as
+  ```
+  induction x
+  · rfl
+  · grind
+  ```
+  -/
+  let tacss2 := eraseTacs tacss2 solvedAll
+  trace[try.debug.chain] "kinds: {getKindsSolvedAll tacss2}"
+  let kinds := getKindsSolvedAll tacss2
+  -- Give preference to tactics of the same kind that solved all subgoals
+  for k in kinds do
+    (_, acc) ← go tacss2 0 [] (some k) |>.run acc
+  -- Remove tactics with kind in `kinds`. Again, we claim mixed kind solutions are suboptimal.
+  let tacss2 := tacss2.map fun s => s.filter fun tac => !kinds.contains tac.raw.getKind
+  if (!acc.isEmpty && tacss2.all fun s => !s.isEmpty)
+     -- We only include partial solutions if there are no other solutions.
+     || (acc.isEmpty && tacss2.any fun s => !s.isEmpty) then
+    (_, acc) ← go tacss2 0 [] none |>.run acc
+  mkTrySuggestions acc
+where
+  go (tacss2 : Array (Array (TSyntax `tactic))) (i : Nat) (acc : List (TSyntax `tactic)) (kind? : Option SyntaxNodeKind) : StateT (Array (TSyntax `tactic)) M Unit := do
+    if (← get).size > (← read).config.max then
+      return ()
+    else if h : i < tacss2.size then
+      if tacss2[i].isEmpty then
+        go tacss2 (i+1) ((← `(tactic| · sorry)) :: acc) kind?
+      else
+        for tac in tacss2[i] do
+          if let some kind := kind? then
+            if tac.raw.getKind == kind then
+              go tacss2 (i+1) ((← `(tactic| · $tac:tactic)) :: acc) kind?
+          else
+            go tacss2 (i+1) ((← `(tactic| · $tac:tactic)) :: acc) kind?
+    else
+      let tac ← `(tactic| · $tac1:tactic
+                            $(acc.toArray.reverse)*)
+      modify (·.push tac)
+
+private def evalSuggestGrindTrace (tac : TSyntax `tactic) : M (TSyntax `tactic) := do
+  match tac with
+  | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    let config ← elabGrindConfig configStx
+    let config := { config with trace := (← read).config.only, verbose := false }
+    let tac ← grindTraceToGrind tac
+    let trace ← evalGrindCore tac config only params fallback?
+    trace[try.debug] "`grind` succeeded"
+    if (← read).config.only then
+      let tac' ← mkGrindOnly configStx fallback? trace
+      mkTrySuggestions #[tac, tac']
+    else
+      return tac
+  | _ => throwUnsupportedSyntax
+
+private def evalSuggestSimpTrace (tac : TSyntax `tactic) : M (TSyntax `tactic) := do (← getMainGoal).withContext do
+  match tac with
+  | `(tactic| simp? $_:optConfig $[only%$only]? $[[$args,*]]? $(loc)?) =>
+    let tac ← simpTraceToSimp tac
+    let { ctx, simprocs, .. } ← mkSimpContext tac (eraseLocal := false)
+    let stats ← simpLocation ctx (simprocs := simprocs) none <| (loc.map expandLocation).getD (.targets #[] true)
+    trace[try.debug] "`simp` succeeded"
+    if (← read).config.only then
+      let tac' ← mkSimpCallStx tac stats.usedTheorems
+      mkTrySuggestions #[tac, tac']
+    else
+      return tac
+  | _ => throwUnsupportedSyntax
+
 @[extern "lean_eval_suggest_tactic"] -- forward definition to avoid mutual block
 opaque evalSuggest (tac : TSyntax `tactic) : M (TSyntax `tactic)
 
@@ -240,7 +269,7 @@ private def evalSuggestChain (tac1 tac2 : TSyntax `tactic) : M (TSyntax `tactic)
   let mut i : Nat := 0
   for goal in goals do
     setGoals [goal]
-    let tac2' : TSyntax `tactic ← (evalSuggest tac2) <|> `(tactic| sorry)
+    let tac2' : TSyntax `tactic ← (evalSuggest tac2) <|> (if (← read).config.missing then `(tactic| sorry) else failure)
     i := i + 1
     tac2s := tac2s.push tac2'
   if tac2s.all isSorry then
@@ -292,6 +321,9 @@ private partial def evalSuggestAttemptAll (tacs : Array (TSyntax ``Parser.Tactic
   go 0 none #[]
 where
   go (i : Nat) (saved? : Option SavedState) (acc : Array (TSyntax `tactic)) : M (TSyntax `tactic) := do
+    -- Remark: we considered using `acc.size < (← read).config.max` here to truncate the search,
+    -- but it had a negative effect when using `<;>`. We could miss a preferred solution `induction e <;> grind`
+    -- because only a subset of the goals were solved by simpler tactics such as `rfl` and `simp`.
     if i < tacs.size then
       match (← observing (evalSuggestTacticSeq tacs[i]!)) with
       | .ok tac s =>
@@ -338,9 +370,12 @@ private def getSuggestions (tac : TSyntax `tactic) : Array Tactic.TryThis.Sugges
   let tacs := getSuggestionsCore tac
   tacs.map toSuggestion
 
-private def throwEvalAndSuggestFailed : TacticM Unit := do
+private def throwEvalAndSuggestFailed (config : Try.Config) : TacticM α := do
   let goal ← getMainGoal
-  Meta.throwTacticEx `«try?» goal "consider using `grind` manually"
+  if config.missing then
+    Meta.throwTacticEx `«try?» goal "consider using `grind` manually"
+  else
+    Meta.throwTacticEx `«try?» goal "consider using `grind` manually, or `try? +missing` for partial proofs containing `sorry`"
 
 private def addSuggestions (tk : Syntax) (s : Array Tactic.TryThis.Suggestion) : TacticM Unit := do
   if s.size == 1 then
@@ -349,10 +384,13 @@ private def addSuggestions (tk : Syntax) (s : Array Tactic.TryThis.Suggestion) :
     Tactic.TryThis.addSuggestions tk (s.map fun stx => stx) (origSpan? := (← getRef))
 
 def evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (config : Try.Config := {}) : TacticM Unit := do
-  let tac' ← evalSuggest tac |>.run { terminal := true, root := tac, config }
-  let s := getSuggestions tac'
+  let tac' ← try
+    evalSuggest tac |>.run { terminal := true, root := tac, config }
+  catch _ =>
+    throwEvalAndSuggestFailed config
+  let s := (getSuggestions tac')[:config.max].toArray
   if s.isEmpty then
-    throwEvalAndSuggestFailed
+    throwEvalAndSuggestFailed config
   else
     addSuggestions tk s
 
@@ -394,7 +432,7 @@ private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
 set_option hygiene false in -- Avoid tagger at `+arith`
 /-- `simp` tactic syntax generator -/
 private def mkSimpStx : CoreM (TSyntax `tactic) :=
-  `(tactic| first | simp?; done | simp? +arith; done | simp_all; done)
+  `(tactic| first | simp? | simp? +arith | simp_all)
 
 /-- `simple` tactics -/
 private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=

src/Lean/Meta/Tactic/Try.lean

@@ -14,5 +14,6 @@ builtin_initialize registerTraceClass `try.collect.funInd
 
 builtin_initialize registerTraceClass `try.debug
 builtin_initialize registerTraceClass `try.debug.funInd
+builtin_initialize registerTraceClass `try.debug.chain
 
 end Lean

tests/lean/run/grind_constProp.lean

@@ -205,18 +205,10 @@ def evalExpr (e : Expr) : EvalM Val := do
 @[grind] theorem UnaryOp.simplify_eval (op : UnaryOp) : (op.simplify a).eval σ = (Expr.una op a).eval σ := by
   grind [UnaryOp.simplify.eq_def]
 
-/--
-info: Try these:
-• (induction e using Expr.simplify.induct) <;> grind
-• ·
-  induction e using Expr.simplify.induct
-  · grind only [Expr.simplify, BinOp.simplify, Expr.eval, BinaryOp.simplify_eval]
-  · grind only [UnaryOp.simplify_eval, UnaryOp.simplify, Expr.simplify, Expr.eval]
-  · simp
--/
+/-- info: Try this: (induction e using Expr.simplify.induct) <;> grind -/
 #guard_msgs (info) in
 example (e : Expr) : e.simplify.eval σ = e.eval σ := by
-  try?
+  try? (max := 1)
 
 @[simp, grind =] theorem Expr.eval_simplify (e : Expr) : e.simplify.eval σ = e.eval σ := by
   induction e, σ using Expr.simplify.induct <;> grind
@@ -312,23 +304,10 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : (
 @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by
   grind
 
-/--
-info: Try these:
-• (induction σ₁, σ₂ using State.join.induct) <;> grind
-• ·
-  induction σ₁, σ₂ using State.join.induct
-  ·
-    grind only [State.join_le_left, State.find?, State.join, State.join_le_left_of, State.le, = State.find?_nil,
-      State.bot_le, State.le_refl]
-  ·
-    grind only [State.join, State.join_le_left, State.length_erase_le, State.find?, State.join_le_left_of, State.le, =
-      State.find?_erase_eq, State.erase_le, State.le_refl, cases Or]
-  · grind only [State.join, State.join_le_left, State.length_erase_le, State.join_le_left_of, State.le, State.erase_le]
-  · grind only [State.join, State.join_le_left, State.length_erase_le, State.join_le_left_of, State.le, State.erase_le]
--/
+/-- info: Try this: (induction σ₁, σ₂ using State.join.induct) <;> grind -/
 #guard_msgs (info) in
 example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
-  try?
+  try? (max := 1)
 
 @[grind] theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
   induction σ₁, σ₂ using State.join.induct <;> grind
@@ -364,7 +343,7 @@ theorem State.erase_le_of_le_cons (h : σ' ≼ (x, v) :: σ) : σ'.erase x ≼
 end
 
 @[grind] theorem Stmt.constProp_correct (h₁ : (σ₁, s) ⇓ σ₂) (h₂ : σ₁' ≼ σ₁) : (σ₁, (s.constProp σ₁').1) ⇓ σ₂ := by
-  induction h₁ generalizing σ₁' <;> try grind [=_ Expr.eval_simplify, intro Bigstep]
+  induction h₁ generalizing σ₁' <;> grind [=_ Expr.eval_simplify, intro Bigstep]
 
 @[grind] def Stmt.constPropagation (s : Stmt) : Stmt :=
   (s.constProp ⊥).1

tests/lean/run/grind_eval_suggest.lean

@@ -60,12 +60,8 @@ example (h : 0 + x = y) : f x = f y := by
 macro "bad_tac" : tactic => `(tactic| eval_suggest (intros; (attempt_all | rfl | grind?); simp))
 
 /--
-error: invalid occurrence of `attempt_all` in non-terminal position for `try?` script
-  (intros;
-    (attempt_all
-      | rfl
-      | grind?);
-    simp)
+error: tactic 'try?' failed, consider using `grind` manually, or `try? +missing` for partial proofs containing `sorry`
+⊢ True
 -/
 #guard_msgs (error) in
 example : True := by

tests/lean/run/grind_try_trace.lean

@@ -23,6 +23,15 @@ info: Try these:
 example : 4 + x + y ≥ 1 + x  := by
   try?
 
+/--
+info: Try these:
+• simp +arith
+• grind
+-/
+#guard_msgs (info) in
+example : 4 + x + y ≥ 1 + x  := by
+  try? -only
+
 /--
 info: Try these:
 • grind
@@ -77,6 +86,13 @@ info: Try these:
 example : app (app as bs) cs = app as (app bs cs) := by
   try?
 
+/--
+info: Try this: (induction as, bs using app.induct) <;> grind [= app]
+-/
+#guard_msgs (info) in
+example : app (app as bs) cs = app as (app bs cs) := by
+  try? (max := 1)
+
 /--
 info: Try these:
 • · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
@@ -106,14 +122,19 @@ def concat : List α → α → List α
 attribute [simp] concat
 
 /--
-info: Try this: ·
+info: Try these:
+• ·
   induction as, a using concat.induct
   · rfl
   · simp_all
+• ·
+  induction as, a using concat.induct
+  · simp
+  · simp_all
 -/
 #guard_msgs (info) in
 example (as : List α) (a : α) : concat as a = as ++ [a] := by
-  try?
+  try? -only
 
 def foo : Nat → Nat
   | 0   => 1
@@ -128,5 +149,14 @@ info: Try this: ·
 -/
 #guard_msgs (info) in
 example : foo x > 0 := by
-  try?  -- `try?` does not solve all subgoals.
+  try? +missing -only -- `try?` does not solve all subgoals.
   sorry
+
+/--
+error: tactic 'try?' failed, consider using `grind` manually, or `try? +missing` for partial proofs containing `sorry`
+x : Nat
+⊢ foo x > 0
+-/
+#guard_msgs (error) in
+example : foo x > 0 := by
+  try?