feat: compress try? suggestions (#6994)

This PR adds the `Try.Config.merge` flag (`true` by default) to the
`try?` tactic. When set to `true`, `try?` compresses suggestions such
as:
```lean
· induction xs, ys using bla.induct
    · grind only [List.length_reverse]
    · grind only [bla]
```
into:
```lean
induction xs, ys using bla.induct <;> grind only [List.length_reverse, bla]
```

This PR also ensures `try?` does not generate suggestions that mixes
`grind` and `grind only`, or `simp` and `simp only` tactics.

This PR also adds the `try? +harder` option (previously called `lib`),
but it has not been fully implemented yet.

src/Init/Try.lean

@@ -15,8 +15,6 @@ structure Config where
   main := true
   /-- If `name` is `true`, all functions in the same namespace are considere for function induction, unfolding, etc. -/
   name := true
-  /-- If `lib` is `true`, uses `libSearch` results. -/
-  lib := true
   /-- If `targetOnly` is `true`, `try?` collects information using the goal target only. -/
   targetOnly := false
   /-- Maximum number of suggestions. -/
@@ -25,6 +23,21 @@ structure Config where
   missing := false
   /-- If `only` is `true`, generates solutions using `grind only` and `simp only`. -/
   only := true
+  /-- If `harder` is `true`, more expensive tactics and operations are tried. -/
+  harder := false
+  /--
+  If `merge` is `true`, it tries to compress suggestions such as
+  ```
+  induction a
+  · grind only [= f]
+  · grind only [→ g]
+  ```
+  as
+  ```
+  induction a <;> grind only [= f, → g]
+  ```
+  -/
+  merge := true
   deriving Inhabited
 
 end Lean.Try

src/Lean/Elab/Tactic/Grind.lean

@@ -174,8 +174,27 @@ def evalGrindCore
     replaceMainGoal []
     return result
 
+/-- Position for the `[..]` child syntax in the `grind` tactic. -/
+def grindParamsPos := 3
+
+/-- Position for the `only` child syntax in the `grind` tactic. -/
+def grindOnlyPos := 2
+
+def isGrindOnly (stx : TSyntax `tactic) : Bool :=
+  stx.raw.getKind == ``Parser.Tactic.grind && !stx.raw[grindOnlyPos].isNone
+
+def setGrindParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic :=
+  if params.isEmpty then
+    ⟨stx.raw.setArg grindParamsPos (mkNullNode)⟩
+  else
+    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
+    ⟨stx.raw.setArg grindParamsPos (mkNullNode paramsStx)⟩
+
+def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
+  stx.raw[grindParamsPos][1].getSepArgs
+
 def mkGrindOnly
-    (config : TSyntax `Lean.Parser.Tactic.optConfig)
+    (config : TSyntax ``Lean.Parser.Tactic.optConfig)
     (fallback? : Option Term)
     (trace : Grind.Trace)
     : MetaM (TSyntax `tactic) := do
@@ -218,11 +237,7 @@ def mkGrindOnly
     `(tactic| grind $config:optConfig only on_failure $fallback)
   else
     `(tactic| grind $config:optConfig only)
-  if params.isEmpty then
-    return result
-  else
-    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
-    return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩
+  return setGrindParams result params
 
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
   match stx with

src/Lean/Elab/Tactic/Simp.lean

@@ -294,6 +294,25 @@ where
               s := s.insert fvarId
       return s
 
+/-- Position for the `[..]` child syntax in the `simp` tactic. -/
+def simpParamsPos := 4
+
+/-- Position for the `only` child syntax in the `simp` tactic. -/
+def simpOnlyPos := 3
+
+def isSimpOnly (stx : TSyntax `tactic) : Bool :=
+  stx.raw.getKind == ``Parser.Tactic.simp && !stx.raw[simpOnlyPos].isNone
+
+def getSimpParams (stx : TSyntax `tactic) : Array Syntax :=
+  stx.raw[simpParamsPos][1].getSepArgs
+
+def setSimpParams (stx : TSyntax `tactic) (params : Array Syntax) : TSyntax `tactic :=
+  if params.isEmpty then
+    ⟨stx.raw.setArg simpParamsPos (mkNullNode)⟩
+  else
+    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
+    ⟨stx.raw.setArg simpParamsPos (mkNullNode paramsStx)⟩
+
 @[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self]
 
 structure MkSimpContextResult where
@@ -321,7 +340,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     if kind == SimpKind.dsimp then
       throwError "'dsimp' tactic does not support 'discharger' option"
   let dischargeWrapper ← mkDischargeWrapper stx[2]
-  let simpOnly := !stx[3].isNone
+  let simpOnly := !stx[simpOnlyPos].isNone
   let simpTheorems ← if simpOnly then
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
@@ -412,8 +431,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
     args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident))
   else
     args := args.push (← `(Parser.Tactic.simpStar| *))
-  let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  return stx.setArg 4 (mkNullNode argsStx)
+  return setSimpParams stx args
 
 def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
   logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"

src/Lean/Elab/Tactic/Try.lean

@@ -169,6 +169,69 @@ def observing (x : M α) : M (TacticResult α) := do
       s.restore (restoreInfo := true)
       return .error ex sNew
 
+private def mergeParams (ps1 ps2 : Array Syntax) : Array Syntax := Id.run do
+  let mut r := ps1
+  for p in ps2 do
+    unless r.contains p do
+      r := r.push p
+  return r
+
+private def mergeSimp? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := Id.run do
+  if setSimpParams tac1 #[] != setSimpParams tac2 #[] then return none
+  let ps1 := getSimpParams tac1
+  let ps2 := getSimpParams tac2
+  return some (setSimpParams tac1 (mergeParams ps1 ps2))
+
+private def mergeGrind? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) := Id.run do
+  if setGrindParams tac1 #[] != setGrindParams tac2 #[] then return none
+  let ps1 := getGrindParams tac1
+  let ps2 := getGrindParams tac2
+  return some (setGrindParams tac1 (mergeParams ps1 ps2))
+
+private def merge? (tac1 tac2 : TSyntax `tactic) : Option (TSyntax `tactic) :=
+  let k := tac1.raw.getKind
+  -- TODO: we can make this extensible by having a command that allows users to register
+  -- `merge?` functions for different tactics.
+  if k == ``Parser.Tactic.simp then
+    mergeSimp? tac1 tac2
+  else if k == ``Parser.Tactic.grind then
+    mergeGrind? tac1 tac2
+  else
+    none
+
+private def mergeAll? (tacs : Array (TSyntax `tactic)) : M (Option (TSyntax `tactic)) := do
+  if !(← read).config.merge || tacs.isEmpty then
+    return none
+  let tac0 := tacs[0]!
+  if tacs.any fun tac => tac.raw.getKind != tac0.raw.getKind then
+    return none
+  let mut tac := tac0
+  for h : i in [1:tacs.size] do
+    let some tac' := merge? tac tacs[i]
+      | return none
+    tac := tac'
+  return some tac
+
+/--
+Returns `true` IF `tacs2` contains only tactics of the same kind, and one of the following
+- contains `simp only ...` and `simp ...`
+- contains `grind only ..` and `grind ...`
+
+We say suggestions mixing `only` and non-`only` tactics are suboptimal and should not be displayed to
+the user.
+-/
+-- TODO: we may add a mechanism for making this extensible.
+private def isOnlyAndNonOnly (tacs2 : Array (TSyntax `tactic)) : Bool := Id.run do
+  if tacs2.isEmpty then return false
+  let k := tacs2[0]!.raw.getKind
+  unless tacs2.all fun tac => tac.raw.getKind == k do return false
+  if k == ``Parser.Tactic.simp then
+    return tacs2.any (isSimpOnly ·) && tacs2.any (!isSimpOnly ·)
+  else if k == ``Parser.Tactic.grind then
+    return tacs2.any (isGrindOnly ·) && tacs2.any (!isGrindOnly ·)
+  else
+    return false
+
 private def mkChainResult (tac1 : TSyntax `tactic) (tacss2 : Array (TSyntax `tactic)) : M (TSyntax `tactic) := do
   let tacss2 := tacss2.map getSuggestionsCore
   if (← isTracingEnabledFor `try.debug) then
@@ -213,17 +276,27 @@ where
       return ()
     else if h : i < tacss2.size then
       if tacss2[i].isEmpty then
-        go tacss2 (i+1) ((← `(tactic| · sorry)) :: acc) kind?
+        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?
+              go tacss2 (i+1) (tac :: acc) kind?
           else
-            go tacss2 (i+1) ((← `(tactic| · $tac:tactic)) :: acc) kind?
+            go tacss2 (i+1) (tac :: acc) kind?
     else
-      let tac ← `(tactic| · $tac1:tactic
-                            $(acc.toArray.reverse)*)
+      let tacs2 := acc.toArray.reverse
+      if kind?.isSome && isOnlyAndNonOnly tacs2 then
+        -- Suboptimal combination. See comment at `isOnlyAndNonOnly`
+        return ()
+      let tac ← if let some tac2 ← mergeAll? tacs2 then
+        -- TODO: when merging tactics, there is a possibility the compressed version will not work.
+        -- TODO: if this is a big issue in practice, we should "replay" the tactic here.
+        `(tactic| $tac1:tactic <;> $tac2:tactic)
+      else
+        let tacs2 ← tacs2.mapM fun tac2 => `(tactic| · $tac2:tactic)
+        `(tactic| · $tac1:tactic
+                    $tacs2*)
       modify (·.push tac)
 
 private def evalSuggestGrindTrace (tac : TSyntax `tactic) : M (TSyntax `tactic) := do
@@ -363,6 +436,8 @@ private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic
           throwError "unsolved goals"
       return r
 
+/-! `evalAndSuggest` frontend -/
+
 private def toSuggestion (t : TSyntax `tactic) : Tactic.TryThis.Suggestion :=
   t
 
@@ -432,11 +507,11 @@ 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? | simp? +arith | simp_all)
+  `(tactic| first | simp? | simp? [*] | simp? +arith | simp? +arith [*])
 
 /-- `simple` tactics -/
 private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
-  `(tactic| attempt_all | rfl | assumption | contradiction)
+  `(tactic| attempt_all | rfl | assumption)
 
 /-! Function induction generators -/
 
@@ -481,7 +556,7 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
   let simple ← mkSimpleTacStx
   let simp ← mkSimpStx
   let grind ← mkGrindStx info
-  let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic)
+  let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all)
   let funInds ← mkAllFunIndStx info atomic
   `(tactic| first | $atomic:tactic | $funInds:tactic)
 

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -158,7 +158,7 @@ def saveFunInd (_e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
 
 open LibrarySearch in
 def saveLibSearchCandidates (e : Expr) : M Unit := do
-  if (← getConfig).lib then
+  if (← getConfig).harder then
     for (declName, declMod) in (← libSearchFindDecls e) do
       unless (← Grind.isEMatchTheorem declName) do
         let kind := match declMod with

tests/lean/run/grind_try_trace.lean

@@ -7,6 +7,7 @@ info: Try these:
 • simp only [ne_eq, reduceCtorEq, not_false_eq_true]
 • grind
 • grind only
+• simp_all
 -/
 #guard_msgs (info) in
 example : [1, 2] ≠ [] := by
@@ -123,18 +124,25 @@ attribute [simp] concat
 
 /--
 info: Try these:
-• ·
-  induction as, a using concat.induct
-  · rfl
-  · simp_all
+• (induction as, a using concat.induct) <;> simp_all
+• (induction as, a using concat.induct) <;> simp [*]
+-/
+#guard_msgs (info) in
+example (as : List α) (a : α) : concat as a = as ++ [a] := by
+  try? -only
+
+/--
+info: Try these:
+• (induction as, a using concat.induct) <;> simp_all
 • ·
   induction as, a using concat.induct
   · simp
-  · simp_all
+  · simp [*]
 -/
 #guard_msgs (info) in
 example (as : List α) (a : α) : concat as a = as ++ [a] := by
-  try? -only
+  try? -only -merge
+
 
 def foo : Nat → Nat
   | 0   => 1
@@ -160,3 +168,21 @@ x : Nat
 #guard_msgs (error) in
 example : foo x > 0 := by
   try?
+
+@[simp] def bla : List Nat → List Nat → List Nat
+  | [],    ys => ys.reverse
+  | _::xs, ys => bla xs ys
+
+attribute [grind] List.length_reverse bla
+
+/--
+info: Try these:
+• (induction xs, ys using bla.induct) <;> grind
+• (induction xs, ys using bla.induct) <;> simp_all
+• (induction xs, ys using bla.induct) <;> simp [*]
+• (induction xs, ys using bla.induct) <;> simp only [bla, List.length_reverse, *]
+• (induction xs, ys using bla.induct) <;> grind only [List.length_reverse, bla]
+-/
+#guard_msgs (info) in
+example : (bla xs ys).length = ys.length := by
+  try?