trivial case of linear_combination

Stream: metaprogramming / tactics

[Heather Macbeth]

Could we arrange for docs#linear_combination with no arguments to be an alias for ring? I think this is a fully coherent interpretation of the linear combination of 0 identities. cc @Abby Goldberg @Rob Lewis

import tactic

variables {x y z w : ℤ} (h₁ : 3 * x = 4 + y) (h₂ : x + 2 * y = 1)

include h₁ h₂

example : 7 * x + z + w = 9 + w + z := by linear_combination (h₁, 2) (h₂, 1) -- works

example : 3 * x - y + z + w = 4 + w + z := by linear_combination (h₁, 1) -- works

example : z + w = w + z := by linear_combination -- the request

[Heather Macbeth]

It could be implemented naively by tossing in ring as the error handling of the case which currently fails with

fail "There are no hypotheses to add"

but I'd guess that it would also be possible to rewrite the logic of the tactic so that this falls out naturally?

[Rob Lewis]

It's just a little bit trickier than you'd expect :sad: it almost works to interpret it as the trivial combination of hypotheses proving 0 = 0. But, which 0 is that? The tactic builds the sum of hypotheses without looking at the target type. You can leave this type as a metavariable to be inferred later, which works. But you also need an add_group instance on it, so at some point after it's inferred you need to call type class inference

[Heather Macbeth]

I see. Would it be terrible to do it this way
Heather Macbeth said:

It could be implemented naively by tossing in ring as the error handling of the case which currently fails with

fail "There are no hypotheses to add"

if the more principled way is difficult?

[Rob Lewis]

Hacky option 1, as you say, is special case the empty list. But then you also have to special case some of the options. (You can disable the normalizer, so what does it mean if you do that and give no hypotheses?)

[Rob Lewis]

Hacky option 2 is to do what I described and check if there's a goal left over that can be solved by apply_instance

[Rob Lewis]

Proper fix, I think, is to get the expected type at the beginning and check that the hypotheses match

[Rob Lewis]

And if there's no hypothesis list given, you can use the expected type to choose which 0 you want

[Rob Lewis]

This has the added benefit of improving error messages if you try to combine hypotheses of different types

[Heather Macbeth]

Thanks for thinking about it! If it seems like a sane and marginally useful addition to you (I was thinking of use in teaching, where it would mean just one fewer thing to cover), can I open an issue for it?

[Rob Lewis]

But it was so close to being a one line change!

[Rob Lewis]

Go for it. It's just beyond what I'm awake enough to do tonight but it won't be hard!

[Heather Macbeth]

#11990 !

[Rob Lewis]

#12062

[Heather Macbeth]

Awesome! Thanks, I'll be glad to have this.