non-terminal `gcongr`?

Stream: mathlib4

[Yoh Tanimoto]

When simp is used in the middle of a proof, it is recommended here to squeeze it. What about other tacics with similar behaviours (that is, they change as more lemmas with attrib are added), such as gcongr?
Should one squeeze it/replace it with explicit terms in the middle of a proof? If not, why?

[Patrick Massot]

gcongr is not meant to be always finishing, so I would say you can use it.

[Michael Rothgang]

You're asking a sharp question here! This has been discussed before (but is not documented elsewhere yet), the keyword is "flexible linter" or "flexible" and "rigid" tactics.

[Michael Rothgang]

This has been implemented as a linter, use set_option linter.flexible true to enable it.

[Michael Rothgang]

(Mathlib doesn't enable that linter by default yet, but complying with it is usually a good idea.)

[Bhavik Mehta]

My opinion (which isn't shared by everyone) is that nonterminal gcongr should have an explicit pattern, since otherwise it's fairly common for it to break if new gcongr lemmas (and positivity extensions) are added

[Sébastien Gouëzel]

When it breaks, it's often because it has become more powerful and that one of the steps of the proof is not necessary anymore. That's good news, and a good occasion to cleanup the proof!

[Bhavik Mehta]

My experience is quite the opposite, it's more common for me that the breakage is of the same form you get with nonterminal simp: the tactic is going further than is useful in a particular application! And so, in my projects, I view unqualified gcongr similarly to nonterminal simp (and I think this is consistent with what the flexible linter thinks)

[Sébastien Gouëzel]

Ah, it's funny we had different feelings. Maybe it's domain-related...

[Yoh Tanimoto]

Thanks to you all for your answers. I understood that, while there's no clear guideline and gcongr can be used in the middle, maybe there are cases where it's reasonable to write explicit terms

[Michael Rothgang]

I don't read Bhavik as saying "write explicit terms", but "use a pattern with gcongr". That should keep some of the robustness, but allows the benefits of using a more powerful tactic (such as, having to write out fewer lemma names by hand).

[Arend Mellendijk]

Does this mean we want a gcongr? tactic like simp? that spits out the pattern that was actually used? I find it quite annoying typing out an explicit pattern.

[Patrick Massot]

You there is already a gcongr? that will help you write the pattern, right?

[Patrick Massot]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Widget/GCongr.html

[Arend Mellendijk]

Ah, so there is! Turns out I wasn't importing that tactic when I tested gcongr? earlier.

[Bhavik Mehta]

Michael Rothgang said:

I don't read Bhavik as saying "write explicit terms", but "use a pattern with gcongr". That should keep some of the robustness, but allows the benefits of using a more powerful tactic (such as, having to write out fewer lemma names by hand).

Yes, this is exactly what I mean!

[Kevin Buzzard]

You can always go suffices [what you want] and then use gcongr of course; this (suffices ... by simpa) used to be a common pattern for "make simp do what you want it to do in a non-fragile way" before we got all the fancy simp? stuff.

[Antoine Chambert-Loir]

I liked the idea that the outcome of such nonfinishing tactics was stored in some way (like says…). This allowed to leave some trace of the expected result that could be useful when some lemmas were added or generalized.

[Bhavik Mehta]

That's exactly what a gcongr pattern would do in this case

[Yury G. Kudryashov]

gcongr? says gcongr _ * ?_ is more informative than gcongr _ * ?_, because it also says "notify me in the CI if gcongr tries to do more".

[Robert Maxton]

Michael Rothgang said:

(Mathlib doesn't enable that linter by default yet, but complying with it is usually a good idea.)

Now that it is enabled by default, what should we do about nonterminal gcongr after simp? Can we register it (or at least gcongr-with-pattern) as a flexible tactic?

[Johan Commelin]

gcongr is quite particular about the goal it expects, right? Especially if you give a pattern.

[Robert Maxton]

Not especially, and depends on the pattern. Unlike, say, rw, where a very specific LHS must appear in the target, gcongr will trigger fine as long as the target is a vaguely symmetric expression with some head it recognizes; within a proof one will likely rewrite many times for every time one changes the head of the proof. For example, if I start the lemma trying to prove, say, s ⊆ t, there's a decent chance that I'll end the lemma still proving something of the form _ ⊆ _.

[Robert Maxton]

In that regard, there's a lot of room for various simp lemmas to trigger or not trigger, but unless a specific 'injectivity'/'monoticity'/etc lemma is added gcongr will continue to work fine; that sounds like a flexible tactic to me.

[Johan Commelin]

From a maintenance pov, I want to know whether it is predictable what the goals will look like. Even if gcongr still succeeds on the new goal, it's unclear whether it still creates the same subgoals as before.
If it suddenly creates 3 subgoals instead of 2, or vice versa, then I wouldn't want to be the person that has to fix that proof.