# Zulip Chat Archive

## 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
_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 (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 :(

#### Yakov Pechersky (Jul 28 2021 at 17:02):

#### 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
_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 (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 `nat`

s, rather than correctly matching on the second line above and matching as `int`

s. 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.

#### Mario Carneiro (Dec 03 2021 at 03:36):

Fixed in #10537

#### Yakov Pechersky (Dec 03 2021 at 05:12):

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

@Mario Carneiro I spent a lot of time trying to follow through `abel`

s 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