abel less powerful than it used to be

Stream: new members

[Christopher Hoskin]

I used (e.g. with lean 3.28.0 and mathlib commit 2ad4a4ce6afc3008272627320370f74cd2020c7f) to be able to do things like:

import algebra.module

universe u

variables (α : Type u) [add_comm_group α]

lemma test (a b c d e f : α) : a-2•b-(c-2•d)-(e-2•f) = a - c -e -2•b+2•d+2•f :=
begin
  abel,
end

and lean would be happy (goals accomplished). However, I recently upgraded to lean 3.31 and mathlib commit 52e6e4cfd8778c6d783c297b361a44e2d9ceca72 and now abel is unable to prove the goal. With exactly the same code it says:

1 goal
α: Type u
_inst_1: add_comm_group α
abcdef: α
⊢ a - 2 • b - (c - 2 • d) - (e - 2 • f) = a + ((-1) • c + (-1) • e) - 2 • b + 2 • d + 2 • f

Is this a regression? Is there some other tactic I should be using now?

Hoping that I don't have to now manually rearrange the brackets and terms as that would be rather tedious!

Christopher

[Ruben Van de Velde]

Hrm, interesting. Could you try simp only [two_smul] before abel?

[Alex J. Best]

This looks like a regression, perhaps its related to #7255?
Note that

import algebra.module

universe u

variables (α : Type u) [add_comm_group α]

lemma test (a b c d e f : α) : a-(2:ℤ)•b-(c-(2:ℤ)•d)-(e-(2:ℤ)•f) = a - c -e -(2:ℤ)•b+(2:ℤ)•d+(2:ℤ)•f :=
begin
  abel,
end

works as intended.

[Christopher Hoskin]

Thanks, this works by rewriting 2•b as b+b before invoking the abel tactic:

import algebra.module

universe u

variables (α : Type u) [add_comm_group α]

lemma test (a b c d e f : α) : a-2•b-(c-2•d)-(e-2•f) = a - c -e -2•b+2•d+2•f :=
begin
  simp only [two_smul],
  abel,
end

But what if I had an equation with 3•b or any larger natural number co-efficient? Is there a way to convert all n:ℕ in an equation to n:ℤ?

[Eric Rodriguez]

lift n to ℤ?

[Eric Rodriguez]

nope, that doesn't work :(

[Yakov Pechersky]

<- docs#gsmul_coe_nat

[Christopher Hoskin]

How would I use gsmul_coe_nat? I tried:

lemma test (a b c d e f : α) : a-2•b-(c-2•d)-(e-2•f) = a - c -e -2•b+2•d+2•f :=
begin
  rw [← gsmul_coe_nat, ← gsmul_coe_nat, ← gsmul_coe_nat],
  abel,
end

But abel still couldn't prove the equation:

1 goal
α: Type u
_inst_1: add_comm_group α
abcdef: α
⊢ a - ↑2 • b - (c - ↑2 • d) - (e - ↑2 • f) = a + ((-1) • c + (-1) • e) - ↑2 • b + ↑2 • d + ↑2 • f

[Kevin Buzzard]

lemma test (a b c d e f : α) : a-2•b-(c-2•d)-(e-2•f) = a - c -e -2•b+2•d+2•f :=
begin
  simp only [← gsmul_coe_nat],
  norm_cast,
  abel,
end

[Christopher Hoskin]

Kevin Buzzard said:

lemma test (a b c d e f : α) : a-2•b-(c-2•d)-(e-2•f) = a - c -e -2•b+2•d+2•f :=
begin
  simp only [← gsmul_coe_nat],
  norm_cast,
  abel,
end

Thanks - that works! I still think it was better when abel did it for me though :)

[Kevin Buzzard]

Did you open an issue on the mathlib github and link to this thread?

[Christopher Hoskin]

@Kevin Buzzard No - but happy to do that if this is a bug rather than new intended behaviour.

[Christopher Hoskin]

GitHub Issue: https://github.com/leanprover-community/mathlib/issues/8456 Thanks for your help.

[Ashley Blacquiere]

I've been doing some exploratory debugging to try to identify the source of this issue (using the mwe proposed by @Rob Lewis in issue 8456). It seems to me that the problem occurs in the pattern match of the eval function in abel (~lines 290 and 291 in abel.lean):

| `(@has_scalar.smul nat _ add_monoid.has_scalar_nat %%e₁ %%e₂) := eval_smul' c eval e₁ e₂
| `(@has_scalar.smul int _ sub_neg_monoid.has_scalar_int %%e₁ %%e₂) :=  eval_smul' c eval e₁ e₂

As noted in Rob's mwe there is a confusion of nat and int types, in particular in smul operations on an add_comm_group: If the scalars are left untyped then abel pattern matches on the first line of code above and recognizes them as nats, rather than correctly matching on the second line above and matching as ints. This is despite the mwe being correctly identified as a group via the context structure.

I think what might be required here is an alternative to the sub_neg_monoid.has_scalar_int pattern match, but I'm not sure how best to proceed from there. I tried the very naive approach of adding has_scalar_int directly to add_comm_group and replacing code in abel as appropriate, but didn't get too far.

I understand some of the more recent changes to abel were in part implemented to handle scalar multiplication similarly across both nat and int (or across groups and monoids), but I don't quite understand how wide ranging these changes might have been, nor how much dependency their might be elsewhere on typeclass instances like sub_neg_monoid.has_scalar_int (I'm assuming more than just abel). That said, does modifying the pattern match with a different typeclass instance seem like the right approach here? Or is there a better way to proceed?

Also, fyi: I'm not necessarily assuming I'll get close enough here to submit a PR for a fix - I expect this might be a bigger problem than I am currently equipped to solve - but it's a helpful exercise for me to better understand metaprogramming.

[Rob Lewis]

At a glance I'm not 100% sure that those instance pattern matches are needed. Replacing them with _ doesn't break any tests, nor does it fix the mwe.

[Rob Lewis]

Could you elaborate on why you think this might be where the issue is? I don't want to say it isn't, but it also doesn't jump out as the problem to me

[Ashley Blacquiere]

Ah... interesting. I did try replacing the nat and int in the two patterns with _, but it did introduce other breakages. I hadn't gone so far as to replace the has_scalar_*in both patterns with _. I see what you mean tho. I've now replaced:

| `(@has_scalar.smul nat _ add_monoid.has_scalar_nat %%e₁ %%e₂) := eval_smul' c eval e₁ e₂
| `(@has_scalar.smul int _ sub_neg_monoid.has_scalar_int %%e₁ %%e₂) :=  eval_smul' c eval e₁ e₂

with:

| `(@has_scalar.smul _ _ _ %%e₁ %%e₂) := eval_smul' c eval e₁ e₂

and the result is the same.

[Rob Lewis]

This is a sneaky bug, in that I can't tell if it's something totally superficial or if it goes deep down to abel's representation of expressions

[Rob Lewis]

If you could even identify what part of the changes #7255 broke the tactic it'd be helpful for debugging

[Ashley Blacquiere]

Interestingly, I don't think any of these patterns are needed either (at least, I've had them commented out, and haven't seen anything else break...)

| `(add_monoid.nsmul %%e₁ %%e₂) := do
  n ← if c.is_group then mk_app ``int.of_nat [e₁] else return e₁,
  (e', p) ← eval $ c.iapp ``smul [n, e₂],
  return (e', c.iapp ``unfold_smul [e₁, e₂, e', p])
| `(sub_neg_monoid.zsmul %%e₁ %%e₂) := do
  guardb c.is_group,
  (e', p) ← eval $ c.iapp ``smul [e₁, e₂],
  return (e', c.app ``unfold_zsmul c.inst [e₁, e₂, e', p])

| `(smul %%e₁ %%e₂) := eval_smul' c eval e₁ e₂
| `(smulg %%e₁ %%e₂) := eval_smul' c eval e₁ e₂

[Rob Lewis]

The abel test suite is tiny and I'm not sure it's comprehensive

[Ashley Blacquiere]

Rob Lewis said:

This is a sneaky bug, in that I can't tell if it's something totally superficial or if it goes deep down to abel's representation of expressions

Ya, that's what I wondered, since it seemed like that match to has_scalar_smul nat was happening before anything else really occurred in abel. It almost seemed more like something to do with an internal representation...

[Ashley Blacquiere]

And I'm not sure my rationale holds up now with the added _... :sweat_smile:

[Ashley Blacquiere]

Rob Lewis said:

If you could even identify what part of the changes #7255 broke the tactic it'd be helpful for debugging

Ok. Good idea. I'll take a closer look to see if I can spot the key issue.

[Ashley Blacquiere]

Actually, it occurs to me that the pattern matches below are for backwards compatibility for any proofs that previously used smul, smulg, nsmul or zsmul.

Ashley Blacquiere said:

Interestingly, I don't think any of these patterns are needed either (at least, I've had them commented out, and haven't seen anything else break...)

| `(add_monoid.nsmul %%e₁ %%e₂) := do
  n ← if c.is_group then mk_app ``int.of_nat [e₁] else return e₁,
  (e', p) ← eval $ c.iapp ``smul [n, e₂],
  return (e', c.iapp ``unfold_smul [e₁, e₂, e', p])
| `(sub_neg_monoid.zsmul %%e₁ %%e₂) := do
  guardb c.is_group,
  (e', p) ← eval $ c.iapp ``smul [e₁, e₂],
  return (e', c.app ``unfold_zsmul c.inst [e₁, e₂, e', p])

| `(smul %%e₁ %%e₂) := eval_smul' c eval e₁ e₂
| `(smulg %%e₁ %%e₂) := eval_smul' c eval e₁ e₂

[Mario Carneiro]

@Ashley Blacquiere not backward compatibility, just plain coverage of the language. Who knows what's in the goal the user gives us; we should support anything that makes sense, otherwise people will not undersand why 1 * 2 = 1 solves fine but smul 1 2 = 1 doesn't even though e.g. rfl works fine

[Mario Carneiro]

Ashley Blacquiere said:

Ah... interesting. I did try replacing the nat and int in the two patterns with _, but it did introduce other breakages. I hadn't gone so far as to replace the has_scalar_*in both patterns with _. I see what you mean tho. I've now replaced:

| `(@has_scalar.smul nat _ add_monoid.has_scalar_nat %%e₁ %%e₂) := eval_smul' c eval e₁ e₂
| `(@has_scalar.smul int _ sub_neg_monoid.has_scalar_int %%e₁ %%e₂) :=  eval_smul' c eval e₁ e₂

with:

| `(@has_scalar.smul _ _ _ %%e₁ %%e₂) := eval_smul' c eval e₁ e₂

and the result is the same.

Without the instance pattern match, the program is slightly unsound. That check is needed to ensure that we are applying the right lemma for the situation, because you can define crazy instances that do different things. Removing the check means that we will always optimistically apply the lemma and leave it to the kernel to notice if they aren't defeq, which works alright but has terrible UX when it goes wrong.

[Mario Carneiro]

Fixed in #10537

[Yakov Pechersky]

#10587

[Ashley Blacquiere]

@Mario Carneiro I spent a lot of time trying to follow through abels logic the last week or so, but based on your fix, I was pretty off-target in terms of where the core issue was... :sweat_smile: The high level explanation that you provided above makes sense, but the details are tricky to follow - especially that last else do block that you added to eval_smul'. I'd really appreciate reading some more detailed documentation on the issue and fix, if you have the time.

[Mario Carneiro]

The attempted fixes, removing and rearranging branches, was never going to work because that particular combination was simply not supported - there was a missing lemma

[Mario Carneiro]

abel uses smulg exclusively for groups, and smul exclusively for monoids, but it's not like one is a specialization of the other, and groups are monoids so it is type correct to use smul on groups

[Mario Carneiro]

so that means that if you have a smul on a group abel has no idea what to do about it because none of the lemmas apply to that situation

[Mario Carneiro]

For the fix, we want to avoid the type error that results from assuming that smul usage exactly matches c.is_group, so we make that two separate booleans. There are four combinations for those bools and two of them (is_smulg = c.is_group = tt and is_smulg = c.is_group = ff) are already handled. The combination is_smulg = tt, c.is_group = ff is impossible because smulg depends on a group parameter (not strictly true since you can have a non-instance group, but we assert it anyway), and in the is_smulg = ff, c.is_group = tt case (that's the else do block), we convert smul a b to smulg a b while descending into it to normalize the pieces. This requires casting a from nat to int, which uses some of norm_num's machinery, copied from eval_cast.

[Rob Lewis]

@Mario Carneiro if you could note this in a comment somewhere it would be great!

[Ashley Blacquiere]

Thanks for that, @Mario Carneiro!