Narrowing the scope of `linear_combination`

Stream: mathlib4

[Heather Macbeth]

I would like to propose narrowing the scope of linear_combination, and this topic is to allow for discussion.

As a reminder: When you are faced with

R : Type u_1
inst✝ : CommRing R
a b c d e f : R
h1 : a * d = b * c
h2 : c * f = e * d
⊢ c * (a * f - b * e) = 0

and write linear_combination e * h1 + a * h2, the tactic:

1. Formally performs the specified operation on the provided hypotheses, i.e. here generates a proof P of the equation

e * (a * d) + a * (c * f) = e * (b * c) + a * (e * d)

2. Forms the expression (goal-LHS - goal-RHS) - (P-LHS - P-RHS) (let's call it E) and applies a lemma which says the goal would follow from showing E is zero
3. Runs ring1 to prove that E = 0.

[Heather Macbeth]

Originally (mathlib3#11646, mathlib3#14229) the only operations supported were adding/subtracting/negating hypotheses and multiplication/division of a hypothesis by a constant. In the port (#605), @Mario Carneiro added some new operations: adding/subtracting a constant to a hypothesis, multiplying two hypotheses together, and dividing by a hypothesis or inverting a hypothesis. I propose disabling these new operations.

[Heather Macbeth]

First, let me argue that we don't lose much: as of #2544 (by @Kyle Miller), the congr(...) syntax now permits the user to form arbitrary operations on hypotheses. So the linear combination in the example above can be written, not too much more inconveniently, as

apply eq_of_add congr(e * $h1 + a * $h2)
ring

and this method also works fine if one wants to consider even wild operations like congr(exp $h1 + $h1 * $h2 - 3).

[Heather Macbeth]

Second, let me argue that we gain something by restricting the scope in this way. One advantage of restricting to genuine linear operations is that it provides implementation robustness. Currently the algorithm is:

1) form the operation on the hypotheses, 2) move everything in this expression and in the goal from RHS to LHS, and finally 3) compare ring-normalized results.

But there's another conceivable implementation:

1) move everything in hypotheses and goal from RHS to LHS, 2) form the operation on the hypotheses, 3) compare ring-normalized results.

Which operations $f$ do the same thing for both implementations? Precisely those for which $f(a_1- b_1, a_2 - b_2, \ldots a_n - b_n)=f(a_1, a_2, \ldots a_n)-f(b_1, b_2, \ldots b_n)$, i.e. ℤ-linear operations.

[Heather Macbeth]

This implementation robustness is useful in its own right (for example, linarith uses the second implementation I described, and I have some ambitions to unify linear_combination more closely with linarith, so it would be convenient to keep open the possibility of switching).

Just as importantly, I believe this implementation robustness is psychologically useful for users. Both are plausible ways to think about this kind of task, and the tactic is made more canonical/predictable/user-friendly by disabling the operations on which they behave differently. Conversely, providing the nonlinear syntax is bad, because there are several plausible guesses for its meaning (does linear_combination h ^ 2 for h : x = y produce a proof of x ^ 2 - y ^ 2 = 0 or (x - y) ^ 2 = 0?).

[Heather Macbeth]

A PR is at #15899. The nonlinear syntax is currently used only twice in the libary.

[Eric Wieser]

To what extent could we drop linear_combination entirely in favor of something like exact mod_ring congr(2*$h1 + $h2)?

[Heather Macbeth]

Is your mod_ring a term elaborator which moves everything to the LHS and then applies ring? And has an optional normalization argument (like linear_combination does) to allow for different normalization tactics?

That term elaborator sounds like it would have the same predictability/user-friendliness issues that I was objecting to in the current linear_combination.

[Eric Wieser]

I think the predictability issue goes away if you take only a single fully-formed expression?

[Heather Macbeth]

Why?

[Eric Wieser]

Because the syntax enforces that the order is "first build the expression, then move everything to the LHS"

[Heather Macbeth]

I think that addresses literal predictability, but not the point I was trying to make about "psychological" predictability.

[Heather Macbeth]

But another obstacle to the exact mod_ring congr(2*$h1 + $h2) idea is that I will shortly be PR-ing linear_combination-for-inequalities, which doesn't allow for a congr(...) implementation.

[Mario Carneiro]

IIRC when we talked about this in Bonn I made the same suggestion as Eric, just move the current linear_combination to something built on top of the congr() term elaborator

[Mario Carneiro]

it would be nice if congr got support for <- h hypotheses though

[Eric Wieser]

Could there be a gcongr() elaborator for the inequality case?

[Jireh Loreaux]

Mario Carneiro said:

it would be nice if congr got support for <- h hypotheses though

What would be the syntax for this exactly? I feel like anywhere I put a ← makes the expression hard to parse. I guess maybe congr($(h₁) + ←$(h₂))?

[Kyle Miller]

You're always free to write congr($h₁ + $h₂.symm)

[Kyle Miller]

I suppose there could be a special case for congr($h₁ + $(← h₂))

[Mario Carneiro]

Kyle Miller said:

I suppose there could be a special case for congr($h₁ + $(← h₂))

that's basically what linear combination is doing

[Heather Macbeth]

Eric Wieser said:

Could there be a gcongr() elaborator for the inequality case?

This would be a huge project, and I don't want to delay linear_combination-for-inequalities for it. (I'm sure you can imagine that it's much easier to support four hard-coded operations than to support arbitrary operations.)

[Heather Macbeth]

But also, I believe it requires a rather subtle adjustment of the gcongr tagging system: since it would reason forward rather than backwards, you'd want to parse and key @[gcongr] lemmas according to what they did to hypotheses, not according to what they did to the goal. It might not even end up being the same class of lemmas.

[Eric Wieser]

My question was more "is this a good longer-term goal?", not "should we build this instead"

[Eric Wieser]

But also, we could reserve the notation gcongr(...) now, but have it only implement those four hard-coded operations to start with!

[Eric Wieser]

It might not even end up being the same class of lemmas.

I guess this is a good argument for not jumping on the name gcongr( though

[Johan Commelin]

@Heather Macbeth I like your narrowing-scope proposal. Will that also make it easier for linear_combination to start working in modules, instead of just rings? You mention $\Z$-linear combinations, but I guess $R$-linear ones could also be in scope right?

• It would need a bit of support for SMul
• You can no longer use ring to cancel all the terms, but hopeful a combination of abel and ring_nf + a bit of extra juice can still work.

[Heather Macbeth]

Can I renew the discussion on this proposal to narrow the scope of linear_combination? As a reminder, the draft PR is #15899, and I have some extensions to linear_combination which I would like to PR once this proposal is settled:

• supporting inequalities
• supporting a self-replacing linarith?-tolinear_combination
• supporting modules (as mentioned by @Johan Commelin -- although to be really useful this also requires a module-normalization tactic, which I will start a separated discussion for [EDIT: here]).

Here is my main argument for narrowing the scope.

The main discussion above so far (from @Eric Wieser and @Mario Carneiro) was about whether linear_combination should be rewritten entirely as a lightweight wrapper for the congr(...) term elaborator -- but as discussed above, this is not compatible with my proposed extension to support inequalities.

[Kyle Miller]

I think it makes sense having more restrictive congruence-like tactics. You're able to do things like propagate types (and improve performance in that way we discovered recently, by elaborating leaf terms) that congr(...) is not suited for. Plus, congr(...) is very general and has no domain-specific knowledge of any kind, and isn't particularly efficient in the way it generates proofs. Users might also write weird non-linear things and not realize it.

If someone wants the power of congr(...), I would suggest making a separate tactic. Perhaps ring_convert h could handle taking an equality h, bring everything to one side, do convert, and try to solve the goal with ring? Then, paired with congr(...), you could write ring_convert congr(2 * $h1 + 3 * $h2) for instance.

[Heather Macbeth]

@Kyle Miller I think I agree with everything you wrote, but just checking, is this intended as an argument for #15899, or against it, or just as a remark?

[Kyle Miller]

It's meant to be a vote in favor :-)

[Patrick Massot]

I don’t have any technical opinion about this. I only want to express my enthusiastic support for any initiative towards having linear_combination for inequalities and a module tactic.

[Heather Macbeth]

@Patrick Massot You can try out linear_combination-for-inequalities and linarith? at branch#HM-linear-combination !

[Patrick Massot]

We really need a cheerleader emoji.

[Patrick Massot]

How can I test? Can I simply use the linear_combination syntax?

[Heather Macbeth]

Yes, you can look at the test file to get started:
https://github.com/leanprover-community/mathlib4/blob/19903e8d9be678a21ec437004fe23e48ff1fcbcf/test/linear_combination.lean#L230-L285

[Eric Wieser]

Re-raising a point from the PR to avoid discussion fragmenting; #15899 also drops support for semirings from linear_combination (and presumably the module version being discussed above doesn't work on semimodules), which I'd argue isn't beneficial.

I think restricting to $\mathbb{N}$-linear operation has the same semantic effect as reducing to $\mathbb{Z}$ linear. Once we restrict things to be linear (which I agree is good), it becomes irrelevant whether everything gets moved to a single subtraction on the LHS or the two sides are handled separately - and so this can now be an implementation detail, preferring the implementation that works most generally.

[Johan Commelin]

I agree that this would be nice to have.

[Heather Macbeth]

I would argue that the current quick'n'dirty mechanism for supporting semirings is not even the best quick'n'dirty mechanism. For example, here are two problems being solved using linear_combination2 (the semiring version) on current Mathlib:

example {a b : ℕ} (h1 : a = b + 4) (h2 : b = 2) : a = 6 := by
  apply add_right_cancel (b := b)
  linear_combination2 h1 + h2

example {a b : ℕ} (h1 : 3 * a = b + 5) (h2 : 2 * a = b + 3) : a = 2 := by
  apply add_right_cancel (b := 2 * a + b + 3)
  linear_combination2 h1 + (←h2)

[Heather Macbeth]

A different semiring mechanism (which I just wrote up) would be to treat "formal subtraction" as addition on the other side of the equation. This is much more user-friendly!

example {a b : ℕ} (h1 : a = b + 4) (h2 : b = 2) : a = 6 := by
  linear_combination h1 + h2

example {a b : ℕ} (h1 : 3 * a = b + 5) (h2 : 2 * a = b + 3) : a = 2 := by
  linear_combination h1 - h2

[Heather Macbeth]

There are also other possible implementations, for example:

• what is done in linarith: don't handle general semirings, but handle ℕ by zify-ing any ℕ equation encountered
• store all coefficients with a boolean flag indicating whether they are "formally positive" or "formally negative"
• if initially working over a cancel-semiring R, search for a ring S which is the "negation closure" of S (basically "additive localization", though I don't know if we have this algebraic theory developed), and transfer all equations from R to S; arrange things so that if R is a true ring then the S produced is just R

[Heather Macbeth]

I would also like to get this* working eventually (since it will be needed to have a full self-replacing linarith?):

example {a b : ℤ} (h1 : a + b = 6) (h2 : a - b = 2) : a = 4 := by
  linear_combination (h1 + h2) / 2

This is an analogous issue, just with division rather than subtraction: one wants a "formal" syntax for the operation even when it is not literally available in the semiring considered.

*Currently you have to write

example {a b : ℤ} (h1 : a + b = 6) (h2 : a - b = 2) : a = 4 := by
  apply mul_right_cancel₀ (b := 2) (by norm_num1)
  linear_combination h1 + h2

[Heather Macbeth]

Heather Macbeth said:

A different semiring mechanism (which I just wrote up) would be to treat "formal subtraction" as addition on the other side of the equation. This is much more user-friendly!

I opened #16103 for this. @Eric Wieser @Johan Commelin is this acceptable to you?

This change makes the tactic more powerful over semirings. It also eliminates the need to support a special syntax for them (which should make it easier to proceed with the other planned refactors).

[Johan Commelin]

@Heather Macbeth Thanks! I like that quite a lot. But I suppose it only works in semirings in which the addition is cancellative? Because those will inject into their "ring closure" (aka additive localization, yadda yadda).

[Heather Macbeth]

That's true. But linear_combination(2) is currently not even used in Mathlib on Nat or NNReal, let alone on a non-cancellative semiring ...

[Patrick Massot]

I forgot to report that I tried on branch#HM-linear-combination

example (x y ε: ℝ) (hx : x ≤ ε/2) (hy : y ≤ ε/2) : x + y ≤ ε := by linear_combination hx + hy

example (x y ε: ℝ) (hx : x ≤ ε/2) (hy : y ≤ ε/4) : x + 2*y ≤ ε := by linear_combination hx + 2*hy

and it makes me very happy. This makes me confident that the current state of this branch is enough for my teaching.

[Eric Wieser]

Heather Macbeth said:

A different semiring mechanism (which I just wrote up) would be to treat "formal subtraction" as addition on the other side of the equation. This is much more user-friendly!

example {a b : ℕ} (h1 : a = b + 4) (h2 : b = 2) : a = 6 := by
  linear_combination h1 + h2

example {a b : ℕ} (h1 : 3 * a = b + 5) (h2 : 2 * a = b + 3) : a = 2 := by
  linear_combination h1 - h2

This is cool, but strikes me as perhaps a little too magic: after new users have tripped over - on Nat everywhere, I think it makes things confusing to then say "oh, except in linear_combination where it actually does mean what you meant"

[Heather Macbeth]

@Eric Wieser Since the existing version (which requires writing

Heather Macbeth said:

example {a b : ℕ} (h1 : a = b + 4) (h2 : b = 2) : a = 6 := by
  apply add_right_cancel (b := b)
  linear_combination2 h1 + h2

example {a b : ℕ} (h1 : 3 * a = b + 5) (h2 : 2 * a = b + 3) : a = 2 := by
  apply add_right_cancel (b := 2 * a + b + 3)
  linear_combination2 h1 + (←h2)

) has literally never been used in Mathlib, it seems worthwhile to me to change to a syntax which is a bit more "magic" ... and a bit less work for the user.

[Heather Macbeth]

By the way, the change also allows polyrith to work on ℕ! Previously, it would fail on the above problems, or on something like

example {a b c d e f : ℕ} (h1 : a * d = b * c) (h2 : e * d = c * f) :
    c * a * f = c * b * e := by
  polyrith

with the error message

polyrith found the following certificate, but it failed to close the goal:
e * h1 - 1 * a * h2

With the change, polyrith solves them without comment.

[Heather Macbeth]

Thinking ahead, can I ask if you also have qualms about this syntax?
Heather Macbeth said:

I would also like to get this* working eventually (since it will be needed to have a full self-replacing linarith?):

example {a b : ℤ} (h1 : a + b = 6) (h2 : a - b = 2) : a = 4 := by
  linear_combination (h1 + h2) / 2

This was what I had planned to have

example {a b : ℤ} (h1 : a + b = 6) (h2 : a - b = 2) : a = 4 := by
  linarith?

self-replace to.

[Eric Wieser]

This one is arguably not problematic, as even integer division would have the right meaning

[Eric Wieser]

So I guess actually linear_combination h1 - h2 is not problematic either, and it would be only -(h2 - h1) that I would (rather weakly) object to (both because the subtraction "should" truncate, and negation doesn't exist on naturals).

[Kyle Miller]

Maybe a weak argument here is that linear_combination is for linear combinations, and truncating subtraction and negation are non-linear.

[Eric Wieser]

Yes, an alternative would be to require the linear_combination2 h1 + (←h2) spelling (edit: or h1 + (h2.symm)?) but teach linear_combination to do cancellation

[Heather Macbeth]

That really seems like a loss to me. We then have to support a separate syntax through several refactors, teach users about this syntax, and teach polyrith and linarith? about this syntax.

[Kyle Miller]

The documentation could say that linear_combination operates as-if the expression is "ring-ified" (i.e., embedded in the enveloping ring)

[Kyle Miller]

Then there's definitely no harm in pretending that - is fine for Nat

[Eric Wieser]

In the generalization where linear_combination works for modules, it would be nice to be able to hover over the -s in the tactic and see which ring / module they belong to

[Heather Macbeth]

I would argue that (←h2) has the advantage of consistency with the treatment of Nat elsewhere in mathlib, but -h2 has the advantage of internal consistency for the tactic itself.

[Kyle Miller]

(Just to clarify my comment three comments up about nonlinearity, I meant it in support of using - here.)

[Eric Wieser]

Sorry for the tangent, but does linear_combination support using something like h1.trans h2 as one of the hypotheses?

[Heather Macbeth]

Yes.

[Eric Wieser]

So the symm version at least comes for free, even if the ← one doesn't?

[Heather Macbeth]

@Eric Wieser Can you expand a bit on this comment? Are you proposing that we allow linear_combination h1 - h2 over Nat, but support neither linear_combination -h nor linear_combination (←h), and instead have the user write linear_combination h.symm?

[Heather Macbeth]

(If so, I could live with this, but as I mentioned above, it seems like a shame to lose the "free" polyrith support for Nat. And it seems like it still wouldn't eliminate potential user confusion: here the tricky point would be explaining that linear_combination supports subtraction but not negation.)

[Yaël Dillies]

I am somewhat with Heather here. The - is cute enough that I am happy for it not to exactly correspond to the operation of the base (semi)ring

[Eric Wieser]

Heather Macbeth said:

Eric Wieser Can you expand a bit on this comment? Are you proposing that we allow linear_combination h1 - h2 over Nat, but support neither linear_combination -h nor linear_combination (←h), and instead have the user write linear_combination h.symm?

Yes, but if this is an unpopular opinion I'm not going to push hard for it. I don't really care about <-, but removing it reduces the amount of syntax to document.

[Rob Lewis]

Heather Macbeth said:

I would argue that (←h2) has the advantage of consistency with the treatment of Nat elsewhere in mathlib, but -h2 has the advantage of internal consistency for the tactic itself.

I think internal consistency for the tactic itself, and simplicity of input notation, are the most important things here!

[Rob Lewis]

(Also very excited to see linarith? coming :tada:)

[Heather Macbeth]

Kyle Miller said:

The documentation could say that linear_combination operates as-if the expression is "ring-ified" (i.e., embedded in the enveloping ring)

I rewrote the documentation as Kyle suggested -- @Eric Wieser hopefully this partially mitigates your concern:
https://github.com/leanprover-community/mathlib4/pull/16103/commits/d3b48e03c894e4216d05a682a8cc7d5ec6788168

[Heather Macbeth]

Can we pick up the linear_combination discussion again? @Eric Wieser can you live with the streamlined syntax proposed in #16103 (for which I count weak support from Johan, Kyle, Yaël and Rob)?

If we can go ahead with #16103, that will unblock #15899, which will unblock the new features!

[Mario Carneiro]

I think it would be easiest if you just moved the old linear_combination out of the way instead of proposing to remove it

[Mario Carneiro]

it makes things awkward when people have to decide between getting a shiny new tactic and removing a potentially useful different tactic

[Heather Macbeth]

@Mario Carneiro Just checking, is this for #16103 or #15899? I believe #16103 is a strict increase in scope (well, except for non-cancellative semirings ...)

[Eric Wieser]

I'll take another look when I'm back from vacation, if someone else doesn't beat me to it

[Mario Carneiro]

@Heather Macbeth both AFAICT

[Mario Carneiro]

my proposal is to do both changes to the original linear_combination, but copy paste the old file and rename the old linear_combination to linear_combination' (and see whether all existing uses can just use the new linear_combination without modification). We can revisit this once people have experienced the various tactics in practice

[Heather Macbeth]

Mario Carneiro said:

(and see whether all existing uses can just use the new linear_combination without modification)

Regarding this: for #16103 yes, for #15899 yes except for two uses.

[Mario Carneiro]

and use linear_combination' for those two uses

[Heather Macbeth]

OK, that seems fine to me. Would you be willing to merge a PR which does that?

[Heather Macbeth]

Also: given that #16103 does not require any changes to mathlib, how do you feel about merging it before the copy-paste operation?

[Mario Carneiro]

I think that would not be a good idea, it's not backward compatible

[Heather Macbeth]

OK, and one more question: how do you feel about doing this

Mario Carneiro said:

IIRC when we talked about this in Bonn I made the same suggestion as Eric, just move the current linear_combination to something built on top of the congr() term elaborator

to shorten linear_combination' after we duplicate?

[Heather Macbeth]

And one more one more question: we could name it compare_mod_ring rather than linear_combination', since it's not linear?

[Mario Carneiro]

The main reason for keeping it with the original name (more or less) is to assist with people upgrading mathlib and debugging a random error in linear_combination they didn't ask for

[Heather Macbeth]

@Mario Carneiro #16166 is the bifurcation PR.

[Notification Bot]

10 messages were moved from this topic to #mathlib4 > Special-casing the unusedTactic linter by Heather Macbeth.

[Heather Macbeth]

Now that the bifurcation is merged, hopefully #16103 is uncontroversial (at least in its general idea -- it still needs a review). I have merged master on it.

[David Ang]

I just discovered this topic from the elliptic curves files --- should I replace the existing legacy linear_combination' with the suggested linear output from polyrith that @Heather Macbeth added in the PR comments?

[Heather Macbeth]

I believe @Mario Carneiro's opinion is that we should leave those two uses on the legacy linear_combination' tactic for now ... then at some later point

Mario Carneiro said:

revisit this once people have experienced the various tactics in practice