abelian failure

Stream: general

[Johan Commelin]

import tactic.abel

universe u

lemma foo (α : Type u) [comm_group α] (b d a c : α) : a * d = d * (b * (a * b⁻¹)) :=
by abel -- abel failed to simplify

lemma bar (α : Type u) [comm_group α] (b d a c : α) : a * d = d * (b * (a * b⁻¹)) :=
begin
  rw mul_comm,
  congr' 1,
  rw mul_left_comm,
  simp,
end

[Johan Commelin]

@Mario Carneiro Do you know what I'm doing wrong here?

[Mario Carneiro]

I think abel was never implemented on multiplicative groups

[Kenny Lau]

aren't they the same as additive groups? [insert mathematician's rant]

[Johan Commelin]

transfer to_additive; abel

[Mario Carneiro]

I think the intent was to use additive to do the translation, and I never got around to it

[Mario Carneiro]

But that better not actually be inverse in a field or I will be annoyed

[Kevin Kappelmann]

Any idea why abel fails for the second example here?

variables {α : Type*} {a : α}
open_locale add_monoid
example [add_comm_monoid α] : 1•a + a = a + a := by abel -- works
example [add_comm_group α] : 1•a + a = a + a := by abel -- fails

[Keeley Hoek]

Note that changing the second abel to repeat { abel } (i.e { abel, abel }) does work

[Kevin Kappelmann]

Interesting. How about this:

example [add_comm_group α] : 2•a - (1•a) = a := by abel -- fails