New tactic for "relational congruence"

Stream: maths

[Heather Macbeth]

I just opened !4#3965, a new tactic (written with @Mario Carneiro) for "relational congruence" reasoning: reducing a relational goal between a LHS and RHS matching the same pattern to relational subgoals between the differing inputs to the pattern. For a quick sense of the style of argument facilitated by the tactic, this commit (which will be PR'd separately) gives >100 examples of use cases in the existing library. Common themes: inequalities, calc blocks, "hard" (as opposed to "soft") analysis.

A typical example is

example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
    x ^ 4 * a + c ≤ x ^ 4 * b + d := by
  rel_congr
  · linarith
  · linarith

This example has the goal of proving the relation ≤ between a LHS and RHS both of the pattern

x ^ 4 * ?_ + ?_

(with inputs a, c on the left and b, d on the right). After the use of rel_congr, we have the simpler goals a ≤ b and c ≤ d.

[Heather Macbeth]

The tactic has various convenience features:

• a pattern can be provided explicitly (same syntax as the mathlib3 congrm tactic), which is convenient if a non-maximal match is desired
• an extensible discharger (currently just wrapping positivity) is run to try to resolve goals identified as "side goals" (for example, the fact 0 ≤ x ^ 4 in the example above)

[Heather Macbeth]

FAQ:

Couldn't Aesop do this?

Aesop is optimized for writing finishing tactics, whereas the crucial use case of this tactic is as a "mid-proof" tactic: cleaning up the goal before the "real proof". An important situation where this matters is when there are several lemmas which match the goal. For example, consider the following two lemmas which both deal with ≤ comparisons between products in ℚ:

theorem mul_le_mul (ha : a1 ≤ a2) (hb : b1 ≤ b2) (hb_pos : 0 ≤ b1) (ha_pos : 0 ≤ a2) :
    a1 * b1 ≤ a2 * b2

theorem mul_le_mul_of_nonneg_left (hb : b1 ≤ b2) (ha_pos : 0 ≤ a) :
    a * b1 ≤ a * b2

The latter lemma only applies to left-constant products (a * b1 ≤ a * b2), but it is strictly more useful in this situation, requiring fewer side conditions. One wants the tactic to prefer the latter lemma in that situation. A finishing tactic doesn't necessarily need a preference: it can just try both and backtrack as needed.

Aesop can support this preference, by assigning a higher priority to the latter lemma (and solve_by_elim, which I used in the prototype implementation, can achieve this by the back door if you tag the lemmas in the right order!), but rel_congr does this in a more principled way: it has a pre-built array of which arguments to the head function * vary between the two sides in the conclusion of the lemmas (so, neglecting implicit arguments, #[true, true] for the first and #[true, false] for the second), and only tries to apply lemmas with the correct array.

The pattern feature rel_congr x ^ 4 * ?_ + _, allowing the user to specify the degree of matching desired, is also an important facet of the tactic's usability as a mid-proof tactic, and it would not be possible to get this from an Aesop implementation.

[Heather Macbeth]

Isn't this just mono?

Yes and no. Both tactics build a tagged family of library lemmas whose conclusions are of the form f [args₁] ∼ f [args₂], and operate by throwing these lemmas at the goal. The closest comparison to rel_congr is actually mono*, the iterating version of mono.

1. rel_congr improves on mono* by including a discharger which attempts to resolve side conditions (whereas the recursion is only run on the main conditions). The mechanism identifying which lemma preconditions are "side" rather than "main" is rather fundamental, and it would require some work to backport this to mono: the "main" antecedents to the lemma are those which are relations between a pair of free variables which occur in matching positions on the LHS and RHS of the conclusion of the lemma.

2. For the issue described above (re: aesop) when a more general and a more specific lemma apply, both rel_congr and mono* are clever enough to prefer the more specific lemma, but their mechanisms are different. The mono* tactic will try to apply both lemmas, and prefer the second by noticing that they both succeed but that the second generates fewer new goals. This is potentially less efficient, as well as less predictable, than the mechanism in rel_congr.

3. The pattern feature rel_congr x ^ 4 * ?_ + _ is new.

4. The philosophy for tagging congruence lemmas is different between @[rel_congr] and @[mono]. For example, both of these lemmas are tagged @[mono]:

   theorem mul_le_mul_of_nonneg_left (hb : b1 ≤ b2) (ha_pos : 0 ≤ a) : a * b1 ≤ a * b2
   
   theorem mul_le_mul_of_nonpos_left (hb : b2 ≤ b1) (ha_neg : a ≤ 0) : a * b1 ≤ a * b2

   In practice, this causes mono* to fail often, printing a message asking for more input from the user (the user then provides syntax such as mono* with b1 ≤ b2). By contrast, rel_congr will run with the first lemma which works, so fewer lemmas should be tagged @[rel_congr] -- the heuristic is to tag only the most likely one for a given situation.

[Kevin Buzzard]

This is a really interesting development! I guess it's going to be slower than just writing the term, but is it still fast?

[Heather Macbeth]

I'll let @Mario Carneiro comment. It's pretty fast.

[Mario Carneiro]

well, things take time, I'm not sure if it's the things we wrote

[Mario Carneiro]

I don't think it should be a very slow tactic. It should be roughly on par with rw

[Heather Macbeth]

I will point out that in addition to being convenient for the author of the code (I hope no one will ever need to memorize the lemma name mul_le_mul_of_nonneg_left again), this tactic should produce proofs which are more comprehensible for the readers of the code, automating a certain class of boilerplate so that the actual ideas stand out better.

Analogy: once you are used to calling the tactic ext, how often have you cared about exactly which extensionality lemmas it is applying?

[Eric Wieser]

for example, both of these lemmas are tagged @[mono]

Which of these lemmas does your new tactic use?

[Eric Wieser]

(and can it be persuaded to use the other one that it doesn't use by default?)

[Yaël Dillies]

This looks like a great tactic. I hope it can replace my idea of having generalised rewrite.

[Joachim Breitner]

I agree! I can see how it can make pen and paper style calc proofs much nicer in some cases.

[Patrick Massot]

This looks really nice! I think this has especially great potential if we could combine it with interface improvements to type calc blocks. On Thursday I ran an intro to Lean afternoon based on a compressed version of the tutorials project but participants were extremely slow to formalize computations, in particular because they had such a hard time getting the calc syntax right. I don't really understand why, but it seems Lean 4 makes this harder, maybe because the underscore leading calc lines is so hard to spot.

[Notification Bot]

10 messages were moved from this topic to #maths > Autogenerating parts of calcs by Heather Macbeth.

[Yury G. Kudryashov]

One issue I had with mono (don't remember Lean version): it was unable to prefer docs#mul_le_mul' (not tagged mono because of this bug) over docs#mul_le_mul for natural numbers.

[Yury G. Kudryashov]

Can your tactic do this?

[Heather Macbeth]

It does by a fluke of tagging order, but it also doesn't matter, because positivity (the discharger) resolves those side goals even if they are created.

[Heather Macbeth]

I also want to bikeshed a bit about tactic naming. I would like this tactic to be called rcongr, placing the emphasis on the congr part, and saving a few characters for something which I hope will be used often (already >100 times if my golfing commit goes through). Currently that name is taken by docs4#Std.Tactic.rcongr, which is used once in the library.

[Heather Macbeth]

/poll Which tactic should get the name rcongr?
Status quo: "repeatedly apply congr and ext"
Proposed change: "relational congr"

[Johan Commelin]

Current rcongr could be renamed to ext_congr, maybe?

[Joachim Breitner]

Does congr_rel relate to congr the same way as rintro to intro and rcases to cases?
If not, I assume there is some confusion that can be avoid by sticking to congr_rel or rel_congr.

[Heather Macbeth]

Neither the status-quo docs4#Std.Tactic.rcongr nor our "relational congr" have the r meaning from rintro/rcases. So maybe you want a third option, "neither"!

[Joachim Breitner]

I was actually tempted to add that. Maybe I should. Did it :-)

[Eric Wieser]

How does this fit in with docs#tactic.interactive.congrm?

[Eric Wieser]

That name would suggest congrr

[Heather Macbeth]

In some sense this tactic is doing congrmr, in that it implements the pattern feature from congrm as well as the relation-handling functionality.

[Eric Wieser]

Would it make sense to just merge it with congrm?

[Eric Wieser]

Which is to say; does rel_congr know how to deal with the = relation by looking at regular congr lemmas?

[Heather Macbeth]

Eric Wieser said:

does rel_congr know how to deal with the = relation by looking at regular congr lemmas?

I'd like that, but it doesn't yet (and nobody ported congrm yet). I don't really know how you get your hands on all the autogenerated congr lemmas.

[Eric Wieser]

Perhaps the compromise for now is to have congrm be essentially:

if head_symbol == Eq then
   do_the_old_congrm
else
   do_the_new_rel_congr

[Eric Wieser]

Recursing back and forth between the two modes might be useful, but certainly isn't necessary in the short term

[Heather Macbeth]

I'd prefer to combine them in that way but under the name rcongr! Because in my opinion the "relational" part is more fundamental than the "match" syntax option. However, let's wait for more opinions.

[Eric Wieser]

It's also possible we could just call them all congr

[Heather Macbeth]

I like that idea, but there are some delicate things that might need to get ironed out. For example, one thing I've really found convenient about congrm is that you can use the pattern-match to force Lean to unfold something it doesn't unfold with congr. I guess it's a difference in the transparency of a certain step in the implementation. Our rel_congr doesn't currently make a transparency distinction according to whether a pattern is present but maybe it should.

[Eric Wieser]

I have some memory that @Kyle Miller made congr more powerful in mathlib4 than it was in mathlib3, though perhaps I'm getting confused with convert

[Kyle Miller]

I added congr! to be more careful and more powerful than the built-in congr tactic (and congr is a bit less powerful than Lean 3's congr, for example it doesn't know about Subsingleton).

congr! aims to do congruence: equating the things on both sides of an equality that correspond to each other. It avoids unfolding definitions to do this since this can be rather unpredictable (though there are some configuration options to make it unfold things in a congr-like way).

I think the way congr unfolds things is sort of accidental. The way it works is it takes the LHS of an equality, generates a congruence lemma, and then applies it to the target. As a consequence, this can make the RHS unfold.

The way congrm takes a pattern that directs how to unfold things is more principled. I suppose it's like a 3-way diff, and the resulting goals are the merge conflicts.

[Kyle Miller]

I changed convert and convert_to to use congr! under the hood, which made it more powerful and (hopefully) a bit easier to predict what it will do.

[Joachim Breitner]

As someone who uses lean only every few months and keeps forgetting everything in between I'd certainly be most happy if there is simply a single congr tactic that I have to know about, and can handle all the cases. If configurable variants on behavior, when they are unavoidable (unfolding or not maybe, if that's unavoidable) are then discoverable from the tooltip, I'm in UX heaven.

[Mario Carneiro]

We really need to figure something out re: forward references to mathlib from core. While it is possible to override tactics, there is no clear single owner for the docstring when an overridden tactic mixes together implementations from several sources.

[Joachim Breitner]

Is the quest for a name for this tactic still going?
You could build on Coq's terminology, call it “generalized congruence”, short gcongr, and start a naming scheme that nicely extends to grewrite and grw and maybe other related tactics that generalize from equality to arbitrary relations, without invading the r… prefix space.

[Heather Macbeth]

I'm ok with gcongr (as the name for the tactic whose working title was rel_congr and whose requested name was, controversially, rcongr). Are there any objections? Perhaps particularly asking @Mario Carneiro, who is the tactic's coauthor :)

[Mario Carneiro]

I have no opinion on this

[Jireh Loreaux]

I have a slight preference for rel_congr because it is a bit more descriptive of the tactic than gcongr.

[Heather Macbeth]

OK, let's do this again ....

[Heather Macbeth]

/poll What shall we name the relational congruence tactic?
rel_congr
rcongr
gcongr

[Heather Macbeth]

Noting that if we choose rcongr,
(1) it requires evicting the current occupant of the name, and
(2) it does not fit the rintros/rcases pattern for the r-prefix.

[Jireh Loreaux]

(oops, sorry Heather, somehow I missed that there was already a poll)

[Heather Macbeth]

There was a poll before, but gcongr hadn't been proposed at that time.

[Patrick Massot]

I think that merging would be more productive than restarting the naming debate.

[Heather Macbeth]

I don't like the current name, so I'm motivated to push for a rename before merge!

[Patrick Massot]

Do you have a favorite name? I would go with that one.

[Heather Macbeth]

OK, I'm going with gcongr, since it's short and the objections raised to it were only aesthetic.

[Heather Macbeth]

Let's live with it for a couple of months and then I don't mind discussing renaming.

[Heather Macbeth]

Hopefully-mature version is awaiting CI at !4#3965.

[Joachim Breitner]

Maybe one day I’ll make meaningful contributions, until then I’ll help with naming :-D

[Joachim Breitner]

I just pulled mathlib into a project of mine and started using gcongr. Works great so far!

I had to add

attribute [gcongr] sub_lt_sub_right add_lt_add_right mul_lt_mul_of_pos_left

first. Is it the case that attributes on relevant lemmas are going to be added to mathlib separately, so in a while I would not have to add these attributes?

[Johan Commelin]

cc @Heather Macbeth

[Mario Carneiro]

Heather has a separate branch which tags a bunch of stuff and golfs proofs in mathlib using it

[Heather Macbeth]

@Joachim Breitner Awesome! Did you import Mathlib.Tactic.GCongr? That should have all these lemmas tagged:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/GCongr.lean

[Heather Macbeth]

Mario Carneiro said:

Heather has a separate branch which tags a bunch of stuff and golfs proofs in mathlib using it

!4#4702

[Joachim Breitner]

No, I did not; I naively assumed that if the tacticgcongr is known, then I would not have to import additional files.
So if I import this file, I don’t have to tag any attribute; in one of my proofs I have to give an explicit pattern (expected), and in another gcongr suddenly used a hypothesis where it didn’t do it before:
https://github.com/nomeata/rerolling-sixes/commit/29e33411090ca7f6b6ef777a56f6d4715f8b2ac5

[Frédéric Dupuis]

This new tactic is great! I just started using it, and I already have some feature requests :-) Is there any chance that the following use case could be supported?

import Mathlib.Analysis.Asymptotics.Asymptotics

variable {α 𝕜 : Type _} [NormedField 𝕜]
variable {l : Filter α}

open Asymptotics

@[gcongr]
lemma IsLittleO.mul_left {f g₁ g₂ : α → 𝕜} (h : g₁ =o[l] g₂) :
    (fun x => f x * g₁ x) =o[l] (fun x => f x * g₂ x) :=
  IsBigO.mul_isLittleO (isBigO_refl _ _) h

Here I get an error on the gcongr attribute, saying that

@[gcongr] attribute only applies to lemmas proving x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got ∀
  {α : Type u_1} {𝕜 : Type u_2} [inst : NormedField 𝕜] {l : Filter α} {f g₁ g₂ : α → 𝕜},
  g₁ =o[l] g₂ → (fun x => f x * g₁ x) =o[l] fun x => f x * g₂ x

I'm guessing this is because fun x => f x * g x is not an Expr.app but rather an Expr.lam, or something like that, but it would be great to support this if it's not too hard.

[Heather Macbeth]

What if you write a defeq variant of the lemma which is in the relational form, like

@[gcongr]
lemma IsLittleO.mul_left {f g₁ g₂ : α → 𝕜} (h : g₁ =o[l] g₂) :
    (f * g₁) =o[l] (f * g₂) :=

This is what we did for big operators and it works pretty well:
https://github.com/leanprover-community/mathlib4/blob/8842682b35b93cd754f489edc823eba1e9b6dc0c/Mathlib/Algebra/BigOperators/Order.lean#L131

[Frédéric Dupuis]

If I do this, it lets me tag the lemma, but then if I try to prove the original lemma by gcongr it doesn't make any progress.

[Jireh Loreaux]

@Heather Macbeth and @Mario Carneiro I absolutely love this tactic! Thanks!

[Heather Macbeth]

@Frédéric Dupuis I see the issue. The head symbols of Finset.sum s f and ∑ x in s, f x (which stands for Finset.sum s (fun x ↦ f x)) are the same, whereas the head symbols of f * g and fun x ↦ f x * g x are different.

[Frédéric Dupuis]

Right. It works if we first transform it into f * g using show, but then this is usually more work than solving the goal manually :-(

[Jireh Loreaux]

Just as a test in what it would take to not use show:

@[gcongr]
lemma IsLittleO.mul_left {f g₁ g₂ : α → 𝕜} (h : g₁ =o[l] g₂) :
    (f * g₁) =o[l] (f * g₂) :=
  IsBigO.mul_isLittleO (isBigO_refl _ _) h

lemma Function.eta (f : β → γ) : (fun x ↦ f x : β → γ) = f := rfl

lemma IsLittleO.mul_left' {f g₁ g₂ : α → 𝕜} (h : g₁ =o[l] g₂) :
    (fun x => f x * g₁ x) =o[l] (fun x => f x * g₂ x) := by
  simp only [←Pi.mul_apply, Function.eta (f * _)]
  gcongr

I'm not saying this is a solution.

[Frédéric Dupuis]

(deleted)

[Yury G. Kudryashov]

I'm going to add @[gcongr] to docs4#Real.rpow_lt_rpow and docs4#Real.rpow_le_rpow. Should I also add it to docs4#Real.rpow_le_rpow_of_exponent_le or we don't want to have opinion about x < 1 vs 1 < x?

[Yury G. Kudryashov]

@Heather Macbeth :up:

[Heather Macbeth]

Thanks! I agree with all three. I think it's better for it to be opinionated, since the template syntax makes it easy to partial-match.

[Yury G. Kudryashov]

OK.

[Heather Macbeth]

You can see in
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/GCongr.lean
that I tagged docs4#pow_le_pow' and docs4#zpow_le_of_le with gcongr, which are the pow and zpow analogues of docs4#Real.rpow_le_rpow_of_exponent_le .