where can I read about `gcongr` (for beginners)?

Stream: new members

[rzeta0]

Where can I read about what the gcongr tactic does and doesn't do?

I'm looking for an explanatory article / video suitable f or beginners.

All I can seem to find online are things like this which are more like source code annotation than explanatory articles:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/GCongr/Core.html

[Rida Hamadani]

https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md#gcongr

[Rida Hamadani]

Oh, apparently this is the same as the docs

[Yury G. Kudryashov]

gcongr takes a goal of the form LHS REL RHS, where REL is a relation like ≤ or ⊆. Then it determines common structure of LHS and RHS. E.g., if the goal is a + b * c ≤ a + x * y, then it will determine _ + ?_ * ?_. Here _ means that the corresponding term is the same on the left and on the right, while ?_ means that the corresponding terms are different. Then it applies lemmas annotated with @[gcongr] attribute (+ some built-in rules) to reduce the goal to something like b ≤ x and c ≤ y, possibly generating side goals like 0 ≤ b. Finally, it tries to discharge the side goals and the new goals using another set of rules (at least positivity for side goals and assumption for main rules, not sure about details).

[Yury G. Kudryashov]

With the current set of rules, it can reduce, e.g., Finset.card (s ∪ t) ≤ Finset.card (s ∪ u) to t ⊆ u.

[rzeta0]

@Yury G. Kudryashov - thanks for explaining.

From what you said, I understood that gcongr would reduce a + b * c ≤ a + x * y down to b * c ≤ x * y, and then decompose into smaller, more manageable, goals, specifically b ≤ x and c ≤ y.

My question is: why not also c ≤ x and b ≤ y?

Is it the case that gcongr tries all combinations? Almost like Prolog tries all combinations to find those that work to meet the overall goal?

[Ruben Van de Velde]

No, it just matches the order

[Ruben Van de Velde]

Have a look at the remaining goals here:

import Mathlib

example (a b c d : ℝ) (h1 : a ≤ c) (h2 : b ≤ d) : a * b ≤ c * d := by
  gcongr

example (a b c d : ℝ) (h1 : a ≤ d) (h2 : b ≤ c) : a * b ≤ c * d := by
  gcongr

[Yury G. Kudryashov]

If you want to prove a * b ≤ c * d in x + a * b ≤ y + c * d using a different lemma than gcongr chooses automatically, then you can use gcongr ?_ + ?_, then make one apply in the goal a * b ≤ c * d and possibly call gcongr again (if a etc are complicated formulae).

[Yury G. Kudryashov]

If you want to make gcongr more clever, then you need to

• come up with a new algorithm;
• discuss it here on Zulip (probably, in the #mathlib4 channel);
• (find someone to) implement it.

[rzeta0]

@Yury G. Kudryashov - I'm actually trying to simplify and reduce the code complexity - preparing educational examples for beginners like myself.

The ideal situation would be if lean4 included a by extra which Heather Macbeth developed for her course "Mechanics of Proof". The readability of the proof is then greatly improved, as is the cognitive load writing such positivity proofs reduced.

[Yury G. Kudryashov]

You can depend on a Heather's repository (or create a repository with her extra tactic, if she didn't publish it as a github repo).