random issue: #2726

Stream: triage

[Random Issue Bot]

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]

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]

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]

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]

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]

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]

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