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.

[Jannis Limperg]

82679d: multiple cosmetic but breaking changes have just landed on Aesop master.

• The syntax for giving options to rule builder has changed from, e.g., @[aesop foo (apply (transparency := reducible))] to @[aesop foo apply (transparency := reducible)].
• The patterns rule builder option (which can be used to restrict cases rules) has been renamed to cases_patterns.
• The (options := { ... }) clause has been renamed to (config := { ... }), for consistency with tactics like simp.
• Similarly, the (simp_options := { ... }) clause has been renamed to (simp_config := { ... }).
• The enabled and useHyps options of simp_config have moved to config and are now called enableSimp and useSimpAll. As a result, simp_config now takes exactly the same options as simp (config := ...).

I'll prepare a Mathlib patch. Apologies to non-Mathlib dependents.

There's also a non-breaking change that might be of interest: Aesop now accepts duplicate clauses in @[aesop], aesop (add ...) and so on. For example, @[aesop safe unsafe 1% ] was previously illegal but now means @[aesop unsafe 1%]. As a result,@[continuity], for example, could now expand to @[aesop safe (rule_sets [Continuity])] and @[continuity unsafe 1%] to @[aesop safe (rule_sets [Continuity]) unsafe 1%].

[Eric Rodriguez]

I don't have the will to fork, but I think the main docstring is out of date: it mentions options := ... still:
https://github.com/leanprover-community/aesop/blob/2f8ec979f3fa425fc219d635e9aa1487c7b09345/Aesop/Frontend/Tactic.lean#L48

[Jannis Limperg]

Fixed on master, thanks!

[Jannis Limperg]

bc4363: Some new convenience features:

• You can now write aesop (add ... (f x)) to add f x as a forward, apply or simp rule. f x stands for an arbitrary term and can contain hypotheses. The parentheses around f x are mandatory.
• You can now write aesop (add ... (by norm_num)) to add a tactic as a rule. norm_num stands for an arbitrary sequence of tactics and can contain hypotheses. Again, the parentheses are mandatory.
• There's a new command add_aesop_rules with the same syntax as the add clause, e.g. add_aesop_rules 1% [(by norm_num), apply f]. This command is particularly useful for adding tactics since, unlike most existing approaches, it works with aesop?.

To enable these features, I had to make one backward-incompatible change: the rule_sets clauses are now written (rule_sets := [...]) instead of (rule_sets [...]). Sorry for the breakage.

Mathlib bump: #10859

[Martin Dvořák]

Are the three dots verbatim?

[Geoffrey Irving]

^ No, they refer to a list of rule set identifiers, like Continuous, Bound.

[Geoffrey Irving]

Or a list of rule features, if you mean the earlier dots.

[Notification Bot]

10 messages were moved from this topic to #lean4 > zetaDelta in Aesop simp by Jannis Limperg.