## Stream: new members

### Topic: abel less powerful than it used to be

#### Christopher Hoskin (Jul 28 2021 at 07:40):

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
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 (Jul 28 2021 at 08:38):

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

#### Alex J. Best (Jul 28 2021 at 11:11):

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 (Jul 28 2021 at 15:33):

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 (Jul 28 2021 at 15:51):

lift n to ℤ?

#### Eric Rodriguez (Jul 28 2021 at 15:52):

nope, that doesn't work :(

#### Christopher Hoskin (Jul 28 2021 at 17:28):

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
abcdef: α
⊢ a - ↑2 • b - (c - ↑2 • d) - (e - ↑2 • f) = a + ((-1) • c + (-1) • e) - ↑2 • b + ↑2 • d + ↑2 • f


#### Kevin Buzzard (Jul 28 2021 at 17:29):

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 (Jul 28 2021 at 17:31):

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 (Jul 28 2021 at 17:31):

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

#### Christopher Hoskin (Jul 28 2021 at 17:33):

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

#### Christopher Hoskin (Jul 28 2021 at 18:15):

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

#### Ashley Blacquiere (Nov 30 2021 at 18:04):

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 (Nov 30 2021 at 18:23):

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 (Nov 30 2021 at 18:23):

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 (Nov 30 2021 at 18:42):

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 (Nov 30 2021 at 18:57):

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 (Nov 30 2021 at 18:58):

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

#### Ashley Blacquiere (Nov 30 2021 at 18:59):

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 (Nov 30 2021 at 18:59):

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

#### Ashley Blacquiere (Nov 30 2021 at 19:00):

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 (Nov 30 2021 at 19:01):

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

#### Ashley Blacquiere (Nov 30 2021 at 19:01):

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 (Dec 03 2021 at 00:17):

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 (Dec 03 2021 at 03:02):

@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 (Dec 03 2021 at 03:07):

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.

Fixed in #10537

#10587

#### Ashley Blacquiere (Dec 03 2021 at 17:25):

@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 (Dec 03 2021 at 17:27):

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 (Dec 03 2021 at 17:28):

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 (Dec 03 2021 at 17:29):

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 (Dec 03 2021 at 17:34):

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 (Dec 03 2021 at 17:39):

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

#### Ashley Blacquiere (Dec 03 2021 at 17:49):

Thanks for that, @Mario Carneiro!

Last updated: Dec 20 2023 at 11:08 UTC