Aesop dev updates

Stream: lean4

[Jannis Limperg]

Since Aesop now has some users (cc @Asta Halkjær From, @Sebastian Ullrich ), I'll log user-facing changes in this topic. Starting with...

9af09347a: Aesop can now be used as a non-terminal tactic. It reports the goals which remain after applying safe rules to the root goal, recursively until no safe rules are applicable. Since this is meant to be used only as a debugging aid, Aesop prints a warning for non-terminal calls, but this can be disabled.

[Jannis Limperg]

In preparation for the paper submission, I recently made a bunch of changes which clean up Aesop's semantics, but will probably break your code (sorry):

• bbe07b: Aesop now depends on std.
• 28b344: the rule index now uses reducible transparency. This means that, for example, an apply rule with conclusion P (x :: xs) will fail on the goal P ([x] ++ xs). See discussion at #lean4 > Discrimination tree lookup.
• 9c4b4d: the builtin introduction rules for product-like types (And, Prod, etc.) are now safe rather than unsafe.
• d96217: safe rules now fail if they generate multiple rule applications (e.g. a safe constructors rule where multiple constructors apply to the goal).
• 6bcfda: the elim builder is now called destruct, for consistency with Isabelle's terminology.

[Jannis Limperg]

• bf3d68: the builtin rules no longer split hypotheses h : P ↔ Q into h1 : P -> Q and h2 : Q -> P. Instead, such hypotheses are now treated as equations via propext (like simp usually does).

[Jannis Limperg]

8cebf2: new feature: aesop? outputs a tactic proof as a Try this: suggestion. The scripts are sometimes still buggy or more cumbersome than necessary, but they work for a large majority of Aesop calls in my test suite.

[Scott Morrison]

Perhaps worth mentioning on this thread: aesop now has many more users. It is imported in mathlib4, and being used (experimentally) in the category theory library as a default for structure fields where tidy used to be used in mathlib3. So far (early days) it looks quite promising.

[Marc Huisinga]

I use it as well and it's amazing when configured correctly. I was able to throw out dozens of tedious proofs each with a single aesop invocation the other day.

[Heather Macbeth]

@Jannis Limperg I'm experimenting with Aesop, it's really cool!

Could you please give a bit of documentation on the simp_options available (as mentioned in the readme)? I'd actually like an option to turn off the simplification step entirely, if that exists.

[Jannis Limperg]

Glad to hear it! The simp_options are a superset of the options supported by simp (i.e. simp (config := { ... })). Currently the only additional option is use_hyps as documented in the README. There's currently no option to turn off the simp rule entirely, but I'll implement one.

[Jannis Limperg]

72610c: you can now write aesop (simp_options := { enabled := false }) to disable the simplification rule entirely (@Heather Macbeth ). To make this less cumbersome, you can define a wrapper like aesop_cat.

[Heather Macbeth]

Thank you! Looking forward to trying it!

[Jannis Limperg]

aea5b4: Aesop now supports local and scoped rules. This required a different implementation strategy for rule sets, which has two additional consequences:

• Aesop rule sets must now be declared in a separate file that then gets imported. (They use initialize internally.)
• When an Aesop rule is erased, e.g. with attribute [-aesop], it is removed only for the current section/file rather than permanently. This brings @[aesop] in line with other erasable attributes and prevents potential issues where the order of import statements could become semantically relevant.