Simple question, but can someone explain the role of the aesop tactic in general, and as it pertains to SimpleGraph?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
SimpleGraph is a definition of a "simple graph" in the mathlib4 library. The API for SimpleGraph uses aesop to help automate some common proof steps.
I'm guessing from your question that you've noticed the command
/--
A variant of the `aesop` tactic for use in the graph library. Changes relative
to standard `aesop`:
- We use the `SimpleGraph` rule set in addition to the default rule sets.
- We instruct Aesop's `intro` rule to unfold with `default` transparency.
- We instruct Aesop to fail if it can't fully solve the goal. This allows us to
use `aesop_graph` for auto-params.
-/
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]))
This sets up a custom wrapper around aesop that uses some additional rules suitable for working for SimpleGraph.
It's not clear from your question whether you've read the README for aesop yet. Perhaps you could do so and then clarify your question if needed?
-
$\begingroup$ Thank you! I'll go ahead and see the README for aesop. I'm not familiar with writing such wrappers, so I guess I was just a bit lost. $\endgroup$ Commented Jun 6, 2023 at 3:46
-
$\begingroup$ Can you please add a link to the
SimpleGraphruleset? Is there a place where aesop rulesets are collected? $\endgroup$– rwstCommented Jun 10 at 11:14