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