chore: add aesop wrappers that pass suggestions (#6044)

Adds `aesop_cat?` `aesop_graph?` and `restrict_tac?`
leanprover-community · Jul 22, 2023 · 8db9f1e · 8db9f1e
1 parent 46f71c6
commit 8db9f1e
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 0 deletions.
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -119,6 +119,13 @@ macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
   (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
 
 /--
+We also use `aesop_cat?` to pass along a `Try this` suggestion when using `aesop_cat`
+-/
+macro (name := aesop_cat?) "aesop_cat?" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop? $c* (options := { introsTransparency? := some .default, terminal := true })
+  (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
+/--
 A variant of `aesop_cat` which does not fail when it is unable to solve the
 goal. Use this only for exploration! Nonterminal `aesop` is even worse than
 nonterminal `simp`.

diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -98,6 +98,15 @@ macro (name := aesop_graph) "aesop_graph" c:Aesop.tactic_clause* : tactic =>
       (options := { introsTransparency? := some .default, terminal := true })
       (rule_sets [$(Lean.mkIdent `SimpleGraph):ident]))
 
+/--
+Use `aesop_graph?` to pass along a `Try this` suggestion when using `aesop_graph`
+-/
+macro (name := aesop_graph?) "aesop_graph?" c:Aesop.tactic_clause* : tactic =>
+  `(tactic|
+    aesop $c*
+      (options := { introsTransparency? := some .default, terminal := true })
+      (rule_sets [$(Lean.mkIdent `SimpleGraph):ident]))
+
 /--
 A variant of `aesop_graph` which does not fail if it is unable to solve the
 goal. Use this only for exploration! Nonterminal Aesop is even worse than

diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean
@@ -79,6 +79,12 @@ macro (name := restrict_tac) "restrict_tac" c:Aesop.tactic_clause* : tactic =>
   aesop $c* (options := { introsTransparency? := some .default, terminal := true })
   (rule_sets [$(Lean.mkIdent `Restrict):ident]))
 
+/-- `restrict_tac?` passes along `Try this` from `aesop` -/
+macro (name := restrict_tac?) "restrict_tac?" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop? $c* (options := { introsTransparency? := some .default, terminal := true })
+  (rule_sets [$(Lean.mkIdent `Restrict):ident]))
+
 example {X : TopCat} {v w x y z : Opens X} (h₀ : v ≤ x) (h₁ : x ≤ z ⊓ w) (h₂ : x ≤ y ⊓ z) : v ≤ y :=
   by restrict_tac