Mathlib/Tactic/GCongr #9393

Stream: mathlib4

[Yury G. Kudryashov]

Hi, why do we have a file with lots of attribute [gcongr] instead of using @[gcongr] near these lemmas?

[Alex J. Best]

To keep the import hierarchy cleaner perhaps? If some of the lemmas are low level and we dont want to import Mathlib/Tactic/GCongr.lean and dependencies in those files

[Yury G. Kudryashov]

Do you mean import Mathlib.Tactic.GCongr.Core?

[Yury G. Kudryashov]

It exports almost nothing.

[Yury G. Kudryashov]

Note that Mathlib.Order.Lattice imports Mathlib.Tactic.GCongr.Core.

[Yury G. Kudryashov]

So, it's available in Mathlib.Algebra.Order.Monoid.Lemmas.

[Yury G. Kudryashov]

I'm going to submit a PR that moves @[gcongr] attributes to relevant files.

[Yury G. Kudryashov]

So that one can use gcongr without exporting linear ordered fields.

[Kyle Miller]

The reason I think I remember @Heather Macbeth mentioning is that it's to make sure the core design of what lemmas should be gcongr lemmas are all in one place.

[Kyle Miller]

This doesn't seem to be in either the PR description or the module docstring though.

[Heather Macbeth]

The last discussion of this was here:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60gcongr.60.20and.20.60positivity.60.20in.20.60Tactic.2ECommon.60

[Heather Macbeth]

Kyle's summary is correct, the issue I had worried about was people wrongly tagging lemmas as gcongr; it seemed to me that if all the base tagging was done in a single file then people adding new lemas would be able to quickly grok the pattern of what gets tagged.

[Heather Macbeth]

But it certainly does mess up the import hierarchy!

[Heather Macbeth]

I don't mind if we decide today is the day to redistribute all those lemmas. gcongr is now used widely enough that the whole library serves as a fairly detailed test set.

[Yury G. Kudryashov]

Also, if a file imports GCongr.Core but doesn't import GCongr, then it looks like @[gcongr] is availbale but gcongr doesn't work.

[Heather Macbeth]

It would be nice, at some point, to have tooling to query the gcongr tagging -- maybe a user command you can run to see the list of lemmas with a certain key, maybe a linter. (Some ideas were discussed on the other thread.). For now we could just open an issue.

[Yury G. Kudryashov]

What should we do about Nat lemmas? They have chances to go to Std4 some day.

[Heather Macbeth]

Actually, I hope that gcongr will move to Std4 some day, too.

[Yury G. Kudryashov]

What stops us from moving it there now? Possible instability? Dependencies? Something else?

[Yaël Dillies]

Doesn't that imply moving positivity too?

[Yaël Dillies]

Moving positivity looks very complicated :frowning:

[Heather Macbeth]

We could still have a basic gcongr in Std4, it will just not be ase useful if positivity isn't moved. But it would already e.g. be full-featured for Nat there.

[Yury G. Kudryashov]

Note that we don't have the algebra/order hierarchy in Std4, so the plan should be to move tactics and add extensions for Nat/Int.

[Yaël Dillies]

Can it be made so that/is it already the case that positivity is a configurable discharger for gcongr?

[Heather Macbeth]

But gcongr is written very generally (e.g. it works for modular arithmetic in an exactly analogous way to inequalities), so putting it in Std would let people configure it downstream for their own use cases.

[Yury G. Kudryashov]

Yaël Dillies said:

Can it be made so that/is it already the case that positivity is a configurable discharger for gcongr?

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/GCongr.lean#L19

[Yaël Dillies]

Not sure how I should read this line. If I understand correctly, that makes positivity be the only possible gcongr discharger?

[Heather Macbeth]

gcongr core imports only this from mathlib:

import Mathlib.Init.Order.Defs
import Mathlib.Tactic.Backtrack
import Mathlib.Tactic.Core

and Backtrack is already PR'd to Std: std4#447, and I think Init.Order.Defs is only used for a discharger so in principle that part could be separated out.

[Eric Rodriguez]

Can we keep the file around fully commented just as some documentation?

[Eric Rodriguez]

As in, just say that these are done properly elsewhere but here's documentation on what makes a good/bad gcongr lemma

[Yury G. Kudryashov]

I suggest that we move GCongr.Core to GCongr

[Yury G. Kudryashov]

And move docs there.

[Heather Macbeth]

I'm not sure I understand, what do you mean by "move docs there"?

[Yury G. Kudryashov]

I mean "merge module docstrings of GCongr and GCongr.Core into the module docstring of the new file, expand it if needed".

[Heather Macbeth]

Oh -- I disagree -- the current docs of GCongr.Core will be suitable for the part which might eventually move to Std, so I think merging the docs in GCongr with that will lead to more work later.

[Yury G. Kudryashov]

OK

[Eric Wieser]

Yury G. Kudryashov said:

What stops us from moving it there now? Possible instability? Dependencies? Something else?

Like many other tactics, positivity depends on Qq which is not available in Std (though all it would take to make it available is a line in the lakefile)

[Yury G. Kudryashov]

I was talking about gcongr.

[Yury G. Kudryashov]

Does it depend on Qq?

[Eric Wieser]

Seemingly not

[Jeremy Tan]

I've got a great reason to merge #9393. I was expecting https://github.com/leanprover-community/mathlib4/pull/9348/commits/8a2670d0af8f43df65d85cdbe026cd81afdb1e15 (or similar) to work in my PR #9348:
max_eq_left (sub_nonneg.mpr <| by gcongr <;> positivity)]
But it did not and I started
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/gcongr.20failure/near/410687628
Yury asked me to add attribute [gcongr] div_le_div_of_le_of_nonneg, which does work, but then I saw #9393 and found out that it alone makes the above line work in #9348 without tagging div_le_div_of_le_of_nonneg, which after all is a duplicate of div_le_div_of_le

[Martin Dvořák]

How can I generate a docs# link to the following page?
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/GCongr/Core.html

[Yaël Dillies]

file#Tactic/GCongr/Core for the source

[Jeremy Tan]

I have left two comments on #9393

[Jeremy Tan]

In particular the leftover Nat lemmas in Tactic.GCongr can be untagged without breaking anything else, so only the declaration of positivity remains

[Jeremy Tan]

As to where to set up positivity as the discharger, that is for another PR

[Jeremy Tan]

Had a think about it. gcongr is not currently used for Nat division anywhere in the library, but the tagged lemmas are used in plenty of places. So we should find places where we can use gcongr for Nat division and replace

[Jeremy Tan]

(i.e. the remaining lemmas in Tactic.GCongr are to be handled the same way as the ones already moved out)

[Yury G. Kudryashov]

@Heather Macbeth Could you please have a look?

[Heather Macbeth]

I'll try to get to it tonight!

[Jireh Loreaux]

I just left a few questions. @Heather Macbeth I'm sure you're busy, but just a friendly reminder to have a look when you get the chance.

[Jeremy Tan]

Will any maintainer review and merge this please?

[Jeremy Tan]

Looking at github comments I believe all questions have been resolved