analogue of local tidy attribute

Stream: mathlib4

[Adam Topaz]

What's the aesop_cat analogue of local attribute [tidy] foobar?

[Matthew Ballard]

I don't think it exists yet

[Adam Topaz]

I'm specifically working on the file category_theory.discrete_category where we have the following:

/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/
meta def _root_.tactic.discrete_cases : tactic unit :=
`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]]

run_cmd add_interactive [``tactic.discrete_cases]

local attribute [tidy] tactic.discrete_cases

[Adam Topaz]

porting the tactic is easy enough, e.g. as

macro (name := discrete_cases) "discrete_cases" : tactic =>
  `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)

[Adam Topaz]

but I don't know how to only activate it locally within aesop_cat

[Matthew Ballard]

Let me conjure up the error it fed me

[Matthew Ballard]

attribute [local aesop safe tactic (rule_sets [CategoryTheory])] Std.Tactic.Ext.extCore'

gives local and scoped Aesop rules are not supported

[Adam Topaz]

yeah that's the same error I got.

[Adam Topaz]

but I wonder if there is some way to simulate this in some other way without modifying aesop itself. @Jannis Limperg any hints?

[Matthew Ballard]

Perhaps you can feed it in the config?

[Matthew Ballard]

Apparently there is this erase_aesop_rules [safe apply foo, bar (rule_sets [A])]

[Matthew Ballard]

You can feed it into aesop call but aesop_cat needs a refactor to accommodate this.

[Matthew Ballard]

!4#2299 has convinced me I need to improve my aesop care and feeding

[Jannis Limperg]

Currently, the only way to get local rules is to declare an Aesop rule set and use it only locally. Local and scoped Aesop rules require specific support from Aesop. This is something I've wanted to do for a while, but I've been putting it off because it's a decently big rewrite of that part of Aesop. But if there's now a need for it, I can do it.

Once Aesop supports local and scoped rules, is there still a need for rule sets? If not, I would like to remove this functionality. CC'ing some people who I know use Aesop: @Marc Huisinga @Frédéric Dupuis @Scott Morrison @Moritz Doll

[Matthew Ballard]

Is there a way to union rule sets?

[Scott Morrison]

Oh, I think rule sets are very helpful when setting up aesop wrapper tactics, e.g. aesop_cat.

[Frédéric Dupuis]

I agree rulesets are very useful to write "specialized" versions of aesop, we definitely don't want to give that up!

[Moritz Doll]

I was about to ask how something like continuity and measurability should work without rulesets. It might be possible to replace them just by calling aesop, but that sounds like a possible performance problem to me.

[Frédéric Dupuis]

Right, especially if we want to try to make these capable of proving statements like ContinuousAt f x, which might require doing things like putting linarith as a last resort unsafe 1% rule to show x is in the right subset.

[Gabriel Ebner]

Once Aesop supports local and scoped rules, is there still a need for rule sets?

I think it's a good design choice to be consistent with simp. And simp supports all three.

[Jannis Limperg]

Okay, thanks everyone for the feedback! I'll follow the simp model then.

[Adam Topaz]

I got the file to build in !4#2326 but I still haven't done any linting. And I also feel like the automation isn't as nice as it should be (given the fact that we can't add to aesop locally just yet as discussed above). Any help to get this file in shape would be much appreciated!

[Matthew Ballard]

In the meantime, I tried adding and then erasing tactics !4#2453 for the rule set. It went pretty well.

[Jannis Limperg]

Local and scoped rules are now supported. Mathlib bump PR: !4#2484