# Zulip Chat Archive

## Stream: triage

### Topic: random issue: #2726

#### Random Issue Bot (Oct 30 2020 at 19:17):

Today I chose issue 2726 for discussion!

**a multiplicative version of the abel tactic**

Created by @Scott Morrison (@semorrison) on 2020-05-18

Labels: feature-request, help wanted, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

#### Alex J. Best (Oct 30 2020 at 19:30):

This is still relevant, I tried it at one point but got bogged down and then lost the branch :confused:. It seems there would be two approaches:

1) modify (duplicate) the codebase to match things like `a*b`

in `eval`

as well as `a+b`

which is already there and carry around typeclasses for comm_group in the `cache`

and a flag saying if we are multiplicative or not .

2) Or have some sort of pre and post processing steps that change goals in multiplicative groups into goals in additive groups, (maybe such things already exist as part of the `to_additive`

machinery) then call the original abel and convert the goal back to multiplicative notation if needed.

The second approach seems way better to me having tried the first.

#### Rob Lewis (Oct 30 2020 at 19:33):

The only proposed change is `+`

to `*`

, right? I think it would be simpler to generalize what exists now to be parametric over an operation and a list of lemma names. (I say this without looking at the implementation.)

#### Alex J. Best (Oct 30 2020 at 19:39):

Right, its quite doable, just work to add the matches, there are a couple of tiny difference between the additive and multiplicative cases like there being no exact analogue of `a-b`

in multiplicative land, but seeing as that isn't the abel normal form of that expression anyway it seems like just an inconvenience rather than requiring major changes.

#### Alex J. Best (Oct 30 2020 at 19:41):

The duplication of monoid and group based lemmas just means there is another factor of 2 in the number of lemmas needed.

#### Alex J. Best (Nov 01 2020 at 18:41):

I'm thinking that turning this into a tactic would be way easier than changing abel that much, I didn't yet find any issues with this approach.

```
import algebra.group.type_tags
import data.real.basic
open additive
example (G:Type)[comm_group G] (a b : G) : a ⁻¹ * b⁻¹ * a*b = 1:=
begin
change -of_mul a + -of_mul b + of_mul a + of_mul b = of_mul 1,
abel,
end
example (G:Type)[comm_group G] (a b : G) (h : a * b = 1) : b * a = 1:=
begin
change of_mul b + of_mul a = of_mul 1,
abel,
change a * b = 1,
exact h,
end
example (G:Type)[comm_group G] (a b : G) (h : b * a = 1) : a * b = 1:=
begin
change of_mul b + of_mul a = of_mul 1 at h,
abel at h,
change a * b = 1 at h,
exact h,
end
example (x y : ℝ) : x * y = y * x :=
begin
change of_mul x + of_mul y = of_mul y + of_mul x,
abel,
end
```

#### Alex J. Best (Nov 01 2020 at 18:44):

And another example

```
example (x y : ℝ) : x^2 * y^3 *x *y = x^3 * y^4 :=
begin
change 2 •ℕ of_mul x + 3 •ℕ of_mul y + of_mul x + of_mul y = 3•ℕ of_mul x + 4 •ℕ of_mul y,
abel,
end
```

Last updated: May 18 2021 at 23:14 UTC