Tactic analysis framework

Stream: mathlib4

[Anne Baanen]

This weekend we got a framework for analyzing tactics merged int Mathlib. This was intended for large-scale tests like "is grind a strict improvement over omega?". But we can also do linting with it, such as warning when two adjacent calls to rw can be merged.

The framework scans for sequences of tactics and calls user-configured passes on the corresponding infotree. Declare a pass by defining a docs#Mathlib.TacticAnalysis.Config that has a @[tacticAnalysis] attribute. (There is also docs#Mathlib.TacticAnalysis.ComplexConfig that tries to do some steps for you, but it is still awkward to use; design suggestions welcome.) Some example passes are already available (currently disabled) in Mathlib: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/TacticAnalysis/Declarations.html

• linarithToGrind, omegaToGrind and ringToGrind are used for developing grind: they report an error when one of those tactics can solve a goal, but grind cannot.
• rwMerge warns when there are two rw calls that can become a single call.
• mergeWithGrind warns when a proof contains tac; grind that could be a single grind call.
• terminalToGrind warns when a sequence of tactic calls (currently of length at least 3) can be replaced with grind.

What other passes can we think of? Maybe continuity to fun_prop?

[Rémy Degenne]

Great! continuity to fun_prop and measurability to fun_prop would be nice. measurability applies in some cases where fun_prop does not, but whenever the replacement is possible it results in a significant speed-up.

[Michael Rothgang]

simp_all to simp is also nice

[Jireh Loreaux]

@Anne Baanen how are macros and autoParams handled? Does your framework track those too, or are they invisible?

[Michael Rothgang]

erw to rw would also be nice

[Michael Rothgang]

Possibly norm_num to simp

[Heather Macbeth]

Two successive simp calls that could be combined?

[Heather Macbeth]

nlinarith to linarith

[Alex Meiburg]

I don't know how desirable this is, but definitely plenty of timeslinarith can go to order, ring, or even just abel.

[Aaron Liu]

Heather Macbeth said:

Two successive simp calls that could be combined?

The problem is sometimes they can't be combined

[Heather Macbeth]

@Aaron Liu Doesn't this framework precisely check whether they can be combined?

[Alex Meiburg]

Aaron, my understanding is that the purpose of this framework is that it allows you to specify, "try the combined simp call and see if that works" (ninja'd)

[Aaron Liu]

I can't tell

[Aaron Liu]

oh it does?

[Aaron Liu]

what happens when you time out?

[Heather Macbeth]

Alex Meiburg said:

I don't know how desirable this is, but definitely plenty of timeslinarith can go to order, ring, or even just abel.

linarith to order is particularly worth catching, since order conveys a lot more information.

[Michael Rothgang]

aesop to simp_all is also nice

[Alex Meiburg]

I don't know if these are problems likely to currently be in Mathlib, but nice "tactic linters" to have would be:

• Using obtain where have would suffice (this one at least a few times)
• Using apply or refine where exact would suffice
• Using tauto where rfl would suffice (potentially risky, if the rfl only works by defeq abuse, but there's a "clean" proof in context?)
• I think many lines matching have[.*]ontrivial could be replaced with a nontriviality tactic.
• Cancelling out by exacts.
  * But not when they're part of suffices ... by exact ..., which would really be suffices ... from ..., but does not feel like such an obvious upgrade.
  * Except that very many suffices ... by exact ... are actually suffices foo by exact bar this, which can often just be apply bar instead.

[Alex Meiburg]

This one is also up to taste, but there a ton of instances in mathlib of the form

by_cases hik : i = k
· subst i

which could with some minimal effort be turned into

rcases em (i = k) with rfl | hik
·

which I think is nicer, personally

[Aaron Liu]

What about docs#eq_or_ne

[Alex Meiburg]

yes, em (i = k) or eq_or_ne i k, either way. Maybe the latter's more readablee

[Yaël Dillies]

Alex Meiburg said:

Using obtain where have would suffice

I dislike these replacements of the form "fast and capable tactic" -> "fast and incapable tactic", because you're effectively making the codebase harder to maintain for no good reason. In this world where obtain is strictly better than have at destructing, I see no reason to use haveto destruct. When have is changed to be as capable as obtain, then we should delete obtain

[Anne Baanen]

Jireh Loreaux said:

Anne Baanen how are macros and autoParams handled? Does your framework track those too, or are they invisible?

It hooks into the linter, so if there are no infotrees about autoParams then they are invisible to tactic analysis. For macros at least, they are visible but consciously filtered out (since many tactic implementations are actually macros over other tactics, and I didn't want to make everyone look for ring1 when they want to do ring). The filtering could be a configurable option if that would be desired. Then you'd need to do your own tactic sequence parsing probably.

[Robin Arnez]

Yaël Dillies schrieb:

I see no reason to use have to destruct

The point is to suggest using have when obtain is used to not destruct I think, e.g.

obtain a := 1

[Alex Meiburg]

Yes, that's what I meant. (I actually didn't know that have destructed products, oops... I've always just used obtain for destructuring products. :slight_smile: )

[Michael Rothgang]

Another "tactic linter": by_contra followed by push_neg could become by_contra!

[Edward van de Meent]

these are some options which are inspired by common golfs... I dont think they have been suggested yet:

• merging lines of intro/intros
• inlining have if it's used at most once and is short enough
• merging intro(s) and refine
• merging refines

[Jireh Loreaux]

Edward van de Meent said:

• inlining have if it's used at most once and is short enough
• merging refines

I worry this may lead to decreased readability.

[Michael Rothgang]

Jireh Loreaux said:

Edward van de Meent said:

• inlining have if it's used at most once and is short enough
• merging refines

I worry this may lead to decreased readability.

Offen, I think it doesn't - but sometimes it surely will. In other words, if this is added, it should be disabled by default and come with a comment explaining the trade-off.

[Eric Wieser]

Should all of this analysis come with profiling? "grind works in place of tac; grind, but is 50% slower" etc?

[Heather Macbeth]

It would be wonderful to have the tool generate "every linarith/gcongr/field_simp/... use in Mathlib" as a test suite, so that we could review things we think are performance improvements to linarith with actual data. Currently our only options are (1) profile individual examples where we see performance problems, (2) read the tea leaves to correlate benchmark performance on Mathlib files with the mix of tactics that appear in those files.

[Kim Morrison]

Eric Wieser said:

Should all of this analysis come with profiling? "grind works in place of tac; grind, but is 50% slower" etc?

@Eric Wieser, it already does. (I mean, you can write tools in this framework that choose not to display this information, but the framework provides it.)

[Kim Morrison]

I think it's best if these tools report only significant slow downs. It's just noise to say "you can replace X with Y, but it is 3% slower".

[Kim Morrison]

@Anne Baanen, is ir possible to write a "simp only squeezer" in this framework? e.g. suppose we have

simp only [X, Y, Z]
some_tactic
simp

very often the X, Y, Z are only there because they are what simp? greedily produces at that step, but in fact some subset don't need to be used before some_tactic succeeds, and can then be absorbed into the terminal simp.

I'm not certain this is technically possible with your current setup, could you let me know?

[Michael Rothgang]

#28802 adds an analysis for continuity/measurability -> fun_prop

[Michael Rothgang]

#28804 adds a few more (still WIP)

[Bolton Bailey]

I would like to advocate: simp only -> simp_rw where possible.

There has been some prior discussion here, note that this might not be a performance benefit.

However, I think the ability to click through individual lemmas in the infoview can be a huge readability / understanding boost, especially when you are not clear on why a theorem is true and you are trying to read Lean to understand.

[Bolton Bailey]

Also simp_rw -> rw, but I would expect this to trigger less often.

[Jovan Gerbscheid]

Also, haveI -> have when the goal is a proposition.

[Ruben Van de Velde]

And maybe have → haveI when it isn't?

[Edward van de Meent]

i just remembered, i don't think combinations like simp; assumption or simp;exact -> simpa have been mentioned yet?

[Jovan Gerbscheid]

Ruben Van de Velde said:

And maybe have → haveI when it isn't?

Although in principle this could lead to exponentially large terms.

[Jovan Gerbscheid]

@Edward van de Meent, I presume you are talking about simpa without a using clause? would prefer simp; exact ... over simpa using ..., because it signifies that the term doesn't need to be simplified.

[Edward van de Meent]

firstly, i didn't mean to specify whether or not there is a using clause, i was merely referring to the general pattern which applies when golfing. Secondly, i don't care about showing if the term needs to be simplified, i care about line count.

[Edward van de Meent]

(#28862 is the linter for merging intro lines)

[Edward van de Meent]

something which could be useful/nice for the docs#Mathlib.TacticAnalysis.ComplexConfig is the ability to separate generating a suggestion from the check making sure that the suggestion is sane (and a proper replacement)... right now, ComplexConfig.test does both at the same time, which can result in an inflation of the registered heartbeatcount for the new suggestion.

[Edward van de Meent]

also, the ability to have code-actions and/or clickable Try This suggestions in the infoview might be useful?

[Thomas Murrills]

We can't use addSuggestion in linters (lean4#4363), but we can use docs#Lean.MessageData.hint ! Maybe that would work here?

[Thomas Murrills]

Hmm, actually, that requires CoreM or some refactoring.

[Thomas Murrills]

Is there a reason tell does not have a monadic return type? It would be awfully convenient for this to be in the highest monad possible, I think! (CommandElabM, as far as I can tell.) (Or at least be on top of IO so that we can save the MetaM state we want from test in out and run e.g. CoreM.)

[Thomas Murrills]

Or, I suppose we can construct the MessageData in test if we must? Is that the intention? (ah, but then we don't have easy access to the ref at which we're logging the message, so I can't imagine this is the intention.)

[Thomas Murrills]

Also, ideally, the argument currentTactic in trigger should be of type TSyntax `tactic! :) Is that possible, or is it prevented by something?

[Edward van de Meent]

i think that's possible, when it gets called i think it already has that type

[Thomas Murrills]

I see that we "dangerously" cast the syntax in TacticInfo to TSyntax `tactic anyway in runPass before passing it to trigger, so hopefully we can stand by this promise. :)

[Thomas Murrills]

So, this is the first I've taken some time to look at this, and: this is amazing, and I'm really excited about it! :D If it's okay, I have two initial thoughts, esp. on the request for design suggestions for the complex config.

[Thomas Murrills]

1. I'm not sure we should handle the end of a sequence by inserting a done, as it breaks the expectation of all tactics having actually been written in source, and may be erroneously counted as a "real" done by linters which care about done! Rather, I think we should either:

• pass in Syntax.missing, which is unambiguous
• change the signature of trigger to take in an Option Syntax
• change the signature of trigger to take in a flag e.g. atEndAfterContinue : Bool and pass in the last syntax again, which allows the behavior to depend on the last syntax in the chain without adjusting the context (which could be useful)
• or, add another field to the complex config called e.g. atEndAfterContinue : ctx -> Syntax -> Option ctx, where we pass back in the last syntax encountered in the chain, and a return value of some c is interpreted as an .acceptance.

To me, the last option feels the most right. It could also have a default value of fun _ _ => none to keep config declarations uncluttered. But these are just the ideas I could come up with. :)

[Thomas Murrills]

(2) I believe it might be nice if test and tell were consolidated somehow. Both take in arguments which are useful to the other: the information on the old tactic behavior is useful for testing and is available before testing, but is only passed to tell. We also might want to log several messages, or log them at specific tactics, so tell might like to have access to the Array Syntax that is available earlier, rather than the synthetic tactic. (Thought: to make logging at the correct position easy, the current ref ought to be set appropriately, so that a simple logWarning is probably correct.)

I think logging is fairly easy, and that we do not necessarily need to funnel the author into producing an Option MessageData. Likewise, we might naturally want to construct our message in a higher monad (as in the case of MessageData.hint); and without MetaM, we cannot really use the MVarIds. The choice of out seems unnecessary, since it is effectively just an interface between test and tell—is there a reason we need an interface at all? Yes, kind of:

As far as I can see, the biggest necessary difference to me seems to be that test must run down in MetaM, whereas tell could conceivably run up in CommandElabM and, crucially, in a different metavarcontext. (Indeed, the TacticInfo nodes only provide enough info for running MetaM, so we do seem to be locked into MetaM there...)

A problem, therefore, seeems to be "which state should I log my message in". This seems to depend on the details of runTactic—I think it's good to keep much of that machinery conveniently hidden from the author! (While generally I'm in favor of flexibility here, I also want to avoid boilerplate and heavy lifting of that sort.)

I have just started thinking about this, so I do not have a (good) idea to offer yet. But I wonder if there is a way to just run one thing in MetaM Unit or CommandElabM Unit (the latter of which would demand an appropriate API to make the sorts of things we typically want to do smoother), while providing the opportunity to easily switch to logging from within the original "final" state if necessary.

[Thomas Murrills]

Small issues:

• I PR'd a fix to log messages on the tactic sequence range, instead of the whole command (the synthetic syntax was picking up position info from the ambient ref): #28919
• There's a tricky issue preventing withSetOptionIn from working as expected: findTacticSeqs only visits trees with syntax whose range is enclosed by the range of the syntax which is passed in. However, due to withSetOptionIn, the syntax passed in is only the syntax nested within set_option ... in <stx>, whereas the ranges recorded in the infotrees are the whole command. Hence, the top-level infotrees are not enclosed in the syntax we're looking at, and we skip them. #28926 fixes this simply by passing in the enclosing syntax.

[Anne Baanen]

Kim Morrison said:

Anne Baanen, is ir possible to write a "simp only squeezer" in this framework? e.g. suppose we have

simp only [X, Y, Z]
some_tactic
simp

very often the X, Y, Z are only there because they are what simp? greedily produces at that step, but in fact some subset don't need to be used before some_tactic succeeds, and can then be absorbed into the terminal simp.

I'm not certain this is technically possible with your current setup, could you let me know?

I don't see any technical objections: in the low-level interface, we are given a list of tactic calls. For each subsequence of the form simpOnly :: tail, where simpOnly has the form `(tactic| simp only $simpArgs) and tail.getLast == `(tactic| simp):

• build a new call to simp only for each subset of the simpArgs
• rebuild a new tactic sequence using a call like let seq ← `(tactic| $(newSimpOnly :: tail).toArray;*)
• call runTactic on the new seq, check if that also closes the goal.

Practical objections exist though: we'd have to check a lot of subsets, running a potentially very long sequence of tactics each time. Maybe we'd delete only the arguments from the simp only that are in fact in the simp set?

[Michael Rothgang]

When #29089 lands, adding a linter for calls to field which could become ring would be nice!