Simple question, but can someone explain the role of the aesop tactic in general, and as it pertains to SimpleGraph?


1 Answer 1


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 =>
    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$
    – Alex Byard
    Jun 6, 2023 at 3:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.