Try this: suffices simpa

Stream: general

[Johan Commelin]

Besides squeezing simps, we should also consider the pattern

suffices "expr after simp" by simpa

Because often it will be shorter, more readable, and possibly more robust

[Damiano Testa]

Sure, should I add that as part of the warning message?

[Johan Commelin]

I think I would love to have a little tactic that replaces a simp call by such a suffices-simpa pattern.

[Johan Commelin]

Using Try this: etc

[Damiano Testa]

Ah, something like suffa?? :lol:

[Johan Commelin]

Right

[Damiano Testa]

Ok, that would not be a linter, though.

[Damiano Testa]

I like the idea, though.

[Johan Commelin]

But ideally it is a very small modification of simp. So that you just add one or two letters to a simp invocation to get the suggestion.

[Damiano Testa]

ssimp, for suffices simp?

[Johan Commelin]

sufsimp, maybe? Or simpsuf??

[Damiano Testa]

Shall we move this discussion to a separate thread, though?

[Damiano Testa]

Looking at the output of the linter, there are very few false positives. Almost by definition, I do not know how many false negatives there are.

[Johan Commelin]

simpa!? could generate a suffices simpa when called in a non-terminal spot

[Notification Bot]

14 messages were moved here from #PR reviews > #11247 non-terminal simp linter by Johan Commelin.

[Damiano Testa]

The part that I see will be tricky with this tactic is getting the syntax of the expected type to print right.

[Eric Wieser]

Could simp? just generate multiple try thiss?

[Mario Carneiro]

This isn't really simp-specific, you could always add a suffices block for any tactic which changes the goal state, or a show to any goal state. This seems like a general tactic code action

[Damiano Testa]

#12006 implements a version of this.

[Damiano Testa]

Although I am starting to wonder whether caching unwieldy squeezes is potentially a better approach. Something like

  simp? [...] says

except that the says part gets written to a cache file and says

• retrieves the cache from file, if it exists, or
• adds it to the file, if it does not.