feat: the 'hint' tactic (#8363)

```
example (h : 1 < 0) : False := by hint
example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint
example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint
example {a b : ℚ} (h : a < b) : ¬ b < a := by hint
example : 37^2 - 35^2 = 72 * 2 := by hint
example : Nat.Prime 37 := by hint
```

Tries out any tactics registered using `register_hint tac`, and reports which ones succeed using the new "Try these: " multiple suggestion widgets. Tactics that close the goal are highlighted in green. Tactics that succeed but don't close the goal display the new subgoals in the widget. If `tac` produces a "Try this: " message, use that instead of `tac`.

I haven't hooked up `aesop` yet, because of leanprover-community/aesop#85. Similarly for `norm_num`.

I would like to parallelize this, but I don't think that needs to happen right away.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>

Mathlib.lean

@@ -3207,6 +3207,7 @@ import Mathlib.Tactic.Have
 import Mathlib.Tactic.HaveI
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
+import Mathlib.Tactic.Hint
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases

Mathlib/Mathport/Attributes.lean

@@ -8,6 +8,3 @@ import Lean.Attributes
 namespace Lean.Attr
 
 initialize substAttr : TagAttribute ← registerTagAttribute `subst "substitution"
-
-initialize hintTacticAttr : TagAttribute ←
-  registerTagAttribute `hint_tactic "A tactic that should be tried by `hint`."

Mathlib/Mathport/Syntax.lean

@@ -48,6 +48,7 @@ import Mathlib.Tactic.Find
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Group
 import Mathlib.Tactic.GuardHypNums
+import Mathlib.Tactic.Hint
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.Inhabit
@@ -160,8 +161,6 @@ open Lean Parser.Tactic
 /- S -/ syntax (name := revertAfter) "revert_after " ident : tactic
 /- S -/ syntax (name := revertTargetDeps) "revert_target_deps" : tactic
 
-/- S -/ syntax (name := hint) "hint" : tactic
-
 /- S -/ syntax (name := rcases?) "rcases?" casesTarget,* (" : " num)? : tactic
 /- S -/ syntax (name := rintro?) "rintro?" (" : " num)? : tactic
 

Mathlib/Tactic.lean

@@ -63,6 +63,7 @@ import Mathlib.Tactic.Have
 import Mathlib.Tactic.HaveI
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
+import Mathlib.Tactic.Hint
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases

Mathlib/Tactic/Common.lean

@@ -4,15 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 
-/-
-This file imports all tactics which do not have significant theory imports,
-and hence can be imported very low in the theory import hierarchy,
-thereby making tactics widely available without needing specific imports.
-
-We include some commented out imports here, with an explanation of their theory requirements,
-to save some time for anyone wondering why they are not here.
--/
-
 -- First import Aesop and Qq
 import Aesop
 import Qq
@@ -54,6 +45,7 @@ import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.Have
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
+import Mathlib.Tactic.Hint
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IrreducibleDef
@@ -112,3 +104,27 @@ import Mathlib.Util.AssertExists
 import Mathlib.Util.CountHeartbeats
 import Mathlib.Util.Imports
 import Mathlib.Util.WhatsNew
+
+/-!
+This file imports all tactics which do not have significant theory imports,
+and hence can be imported very low in the theory import hierarchy,
+thereby making tactics widely available without needing specific imports.
+
+We include some commented out imports here, with an explanation of their theory requirements,
+to save some time for anyone wondering why they are not here.
+-/
+
+/-!
+# Register tactics with `hint`.
+-/
+
+section Hint
+
+register_hint split
+register_hint intro
+register_hint aesop
+register_hint decide
+register_hint simp_all?
+register_hint exact?
+
+end Hint

Mathlib/Tactic/Hint.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Std.Tactic.TryThis
+import Std.Linter.UnreachableTactic
+import Mathlib.Data.Nondet.Basic
+import Mathlib.Tactic.FailIfNoProgress
+import Mathlib.Mathport.Rename
+
+/-!
+# The `hint` tactic.
+
+The `hint` tactic tries the kitchen sink:
+it runs every tactic registered via the `register_hint tac` command
+on the current goal, and reports which ones succeed.
+
+## Future work
+It would be nice to run the tactics in parallel.
+-/
+
+open Lean Elab Tactic
+
+open Std.Tactic.TryThis
+
+namespace Mathlib.Tactic.Hint
+
+/-- An environment extension for registering hint tactics. -/
+initialize hintExtension : SimplePersistentEnvExtension (TSyntax `tactic) (List (TSyntax `tactic)) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.cons)
+    addImportedFn := mkStateFromImportedEntries (·.cons) {}
+  }
+
+/-- Register a new hint tactic. -/
+def addHint (stx : TSyntax `tactic) : CoreM Unit := do
+  modifyEnv fun env => hintExtension.addEntry env stx
+
+/-- Return the list of registered hint tactics. -/
+def getHints : CoreM (List (TSyntax `tactic)) := return hintExtension.getState (← getEnv)
+
+open Lean.Elab.Command in
+/--
+Register a tactic for use with the `hint` tactic, e.g. `register_hint simp_all`.
+-/
+elab (name := registerHintStx) "register_hint" tac:tactic : command => liftTermElabM do
+  -- remove comments
+  let tac : TSyntax `tactic := ⟨tac.raw.copyHeadTailInfoFrom .missing⟩
+  addHint tac
+
+initialize
+  Std.Linter.UnreachableTactic.ignoreTacticKindsRef.modify fun s => s.insert ``registerHintStx
+
+/--
+Construct a suggestion for a tactic.
+* Check the passed `MessageLog` for an info message beginning with "Try this: ".
+* If found, use that as the suggestion.
+* Otherwise use the provided syntax.
+* Also, look for remaining goals and pretty print them after the suggestion.
+-/
+def suggestion (tac : TSyntax `tactic) (msgs : MessageLog := {}) : TacticM Suggestion := do
+  -- TODO `addExactSuggestion` has an option to construct `postInfo?`
+  -- Factor that out so we can use it here instead of copying and pasting?
+  let goals ← getGoals
+  let postInfo? ← if goals.isEmpty then pure none else
+    let mut str := "\nRemaining subgoals:"
+    for g in goals do
+      let e ← PrettyPrinter.ppExpr (← instantiateMVars (← g.getType))
+      str := str ++ Format.pretty ("\n⊢ " ++ e)
+    pure (some str)
+  let style? := if goals.isEmpty then some .success else none
+  let msg? ← msgs.toList.findM? fun m => do pure <|
+    m.severity == MessageSeverity.information && (← m.data.toString).startsWith "Try this: "
+  let suggestion ← match msg? with
+  | some m => pure <| SuggestionText.string (((← m.data.toString).drop 10).takeWhile (· != '\n'))
+  | none => pure <| SuggestionText.tsyntax tac
+  return { suggestion, postInfo?, style? }
+
+/-- Run a tactic, returning any new messages rather than adding them to the message log. -/
+def withMessageLog (t : TacticM Unit) : TacticM MessageLog := do
+  let initMsgs ← modifyGetThe Core.State fun st => (st.messages, { st with messages := {} })
+  t
+  modifyGetThe Core.State fun st => (st.messages, { st with messages := initMsgs })
+
+/--
+Run a tactic, but revert any changes to info trees.
+We use this to inhibit the creation of widgets by subsidiary tactics.
+-/
+def withoutInfoTrees (t : TacticM Unit) : TacticM Unit := do
+  let trees := (← getInfoState).trees
+  t
+  modifyInfoState fun s => { s with trees }
+
+/--
+Run all tactics registered using `register_hint`.
+Print a "Try these:" suggestion for each of the successful tactics.
+
+If one tactic succeeds and closes the goal, we don't look at subsequent tactics.
+-/
+-- TODO We could run the tactics in parallel.
+-- TODO With widget support, could we run the tactics in parallel
+--      and do live updates of the widget as results come in?
+def hint (stx : Syntax) : TacticM Unit := do
+  let tacs := Nondet.ofList (← getHints)
+  let results := tacs.filterMapM fun t : TSyntax `tactic => do
+    if let some msgs ← observing? (withMessageLog (withoutInfoTrees (evalTactic t))) then
+      return some (← getGoals, ← suggestion t msgs)
+    else
+      return none
+  let results ← (results.toMLList.takeUpToFirst fun r => r.1.1.isEmpty).asArray
+  let results := results.qsort (·.1.1.length < ·.1.1.length)
+  addSuggestions stx (results.map (·.1.2))
+  match results.find? (·.1.1.isEmpty) with
+  | some r =>
+    -- We don't restore the entire state, as that would delete the suggestion messages.
+    setMCtx r.2.term.meta.meta.mctx
+  | none => admitGoal (← getMainGoal)
+
+/--
+The `hint` tactic tries every tactic registered using `register_hint tac`,
+and reports any that succeed.
+-/
+syntax (name := hintStx) "hint" : tactic
+
+@[inherit_doc hintStx]
+elab_rules : tactic
+  | `(tactic| hint%$tk) => hint tk
+
+end Mathlib.Tactic.Hint

Mathlib/Tactic/Linarith.lean

@@ -1,2 +1,14 @@
+/-
+Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Y. Lewis
+-/
 import Mathlib.Tactic.Linarith.Frontend
 import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Hint
+
+/-!
+We register `linarith` with the `hint` tactic.
+-/
+
+register_hint linarith

Mathlib/Tactic/Linarith/Frontend.lean

@@ -402,9 +402,6 @@ elab_rules : tactic
           (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabTerm ·.raw none)).toList
           ((← elabLinarithConfig (mkOptionalNode cfg)).updateReducibility bang.isSome)
 
--- TODO restore this when `hint` is ported.
--- add_hint_tactic "linarith"
-
 -- TODO restore this when `add_tactic_doc` is ported
 -- add_tactic_doc
 -- { name       := "linarith",
@@ -426,9 +423,6 @@ elab_rules : tactic
         (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabTerm ·.raw none)).toList
         (cfg.updateReducibility bang.isSome)
 
--- TODO restore this when `hint` is ported.
--- add_hint_tactic "nlinarith"
-
 -- TODO restore this when `add_tactic_doc` is ported
 -- add_tactic_doc
 -- { name       := "nlinarith",

scripts/lint-style.py

@@ -254,7 +254,7 @@ def regular_check(lines, path):
         if copy_done and line == "\n":
             continue
         words = line.split()
-        if words[0] != "import" and words[0] != "/-!" and words[0] != "#align_import":
+        if words[0] != "import" and words[0] != "--" and words[0] != "/-!" and words[0] != "#align_import":
             errors += [(ERR_MOD, line_nr, path)]
             break
         if words[0] == "/-!":

test/hint.lean

@@ -0,0 +1,53 @@
+import Mathlib.Tactic.Common
+import Mathlib.Tactic.Linarith
+import Mathlib.Data.Nat.Prime
+
+/--
+info: Try these:
+• linarith
+-/
+#guard_msgs in
+example (h : 1 < 0) : False := by hint
+
+/--
+info: Try these:
+• exact f p
+-/
+#guard_msgs in
+example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint
+
+/--
+info: Try these:
+• simp_all only [and_self]
+-/
+#guard_msgs in
+example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint
+
+/--
+info: Try these:
+• linarith
+-/
+#guard_msgs in
+example {a b : ℚ} (h : a < b) : ¬ b < a := by hint
+
+/--
+info: Try these:
+• exact rfl
+-/
+#guard_msgs in
+example : 37^2 - 35^2 = 72 * 2 := by hint
+
+/--
+info: Try these:
+• simp_all only
+-/
+#guard_msgs in
+example : Nat.Prime 37 := by hint
+
+/--
+info: Try these:
+• aesop
+• simp_all only [zero_le, and_true]
+-/
+#guard_msgs in
+example {P : Nat → Prop} (h : { x // P x }) : ∃ x, P x ∧ 0 ≤ x := by hint