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