customizing tidy

Stream: general

[Reid Barton]

@Scott Morrison I used your tidy tactic to automatically generate a bunch of continuity proofs that I was formerly writing out manually like

continuous_subtype_mk _ $
  continuous_max
    (continuous_mul continuous_const (continuous.comp (continuous.comp continuous_fst continuous_subtype_val) continuous_norm))
    (continuous_sub continuous_const (continuous.comp continuous_snd continuous_subtype_val))

However, in order to make it run in a reasonable amount of time, I had to create a custom version of tidy that only uses a small number of the tactics (I don't need anything even as fancy as dsimp).

[Reid Barton]

Do you have any thoughts about making tidy easier to customize like this? I see that there's an option for adding tactics to the list that tidy uses, but to remove tactics I had to copy the definition of tidy.

[Reid Barton]

Maybe just a matter of making tidy a bit more modular at the source level

[Scott Morrison]

That's a good idea. How about I just pass the list of tactics as a configuration variable, and then in different contexts people can provide a wrapper tactic that installs their preferred list?

[Reid Barton]

Yes, I think that would be simplest.

[Scott Morrison]

Maybe I'll rename it generic_tidy, to allow specialised variants to still be called tidy. (An alternative would be that specialised variations be called category_tidy or topology_tidy, etc.)

[Reid Barton]

Another feature I can imagine wanting is to have separate applicable and tidyattributes for different "instances" of tidy (e.g., I might want my continuity tactic to only apply the lemmas that prove continuity), but I haven't found just having a single set to be an actual problem yet.

[Scott Morrison]

My plan with my Lean time at the moment is to 1) get a PR for a small fraction of my category theory library ready, with no automation, 2) try to get my automation into mathlib, 3) get the rest of the category theory library in, with automation

[Scott Morrison]

Okay --- are there parameters for attributes? I haven't really explored this.

[Reid Barton]

I've seen attributes that appear to take arguments

[Scott Morrison]

My inclination though is that this can wait, and namespacing is a better solution: just make sure only the things you want to have tidy use are actually in scope.

[Scott Morrison]

Also -- a lot of applicable will be removed after I get to my "use ext" TODO.

[Scott Morrison]

But it will still be needed in places.

[Reid Barton]

Definitely it can wait.
Is applicable affected by namespacing? I hadn't realized that

[Reid Barton]

I mean, by which namespaces are open; as opposed to just what files have been imported (which is generally "pretty much everything")

[Scott Morrison]

Oh, actually you're probably right, and that it ignores namespacing. At some point I'll investigate whether that is good or bad!

[Scott Morrison]

Okay, there's a new commit of lean-tidy, that now allows calling tidy { tactics := [ ... ] }, to replace my default (carefully curated!) list of tactics.

[Scott Morrison]

I'd also be very happy to try to improve my list so it also works on your continuity problems. Having the best possible "out of the box" tidying is nice. :-)