add_comm_group tactic?

Stream: Is there code for X?

[Kevin Buzzard]

Is there a tactic which does this?

example (A : Type) [add_comm_group A] (a b c : A) :
a = -b - c + (a + b + c) :=
begin
  sorry
end

I thought ac_refl would do it but it can't handle the subtraction as far as I can see. Sure I know that one can prove it by looking up all the necessary lemmas needed to remove the subtractions, but a beginner can't do this without a lot of help.

[Johan Commelin]

Doesn't abel do this?

[Kevin Buzzard]

Yes! thanks! I remember the time people were talking about writing this but I didn't know it was written.

[Scott Morrison]

Afaik, we still don't have a noncomm_abel. It should be very easy; just an even smaller version of tactic#noncomm_ring

[Scott Morrison]

(Obviously it would not be called noncomm_abel...)

[Jalex Stark]

@Scott Morrison are you talking about the tactic patrick wrote in #3062? it's just waiting on review

[Utensil Song]

@Kevin Buzzard Thanks a lot!

I did try tactic#ring many times (since in my case, it's also a ring) because I assumed that tactic#ring is more powerful than tactic#abel, but tactic#ring could not solve this #mwe :

example (A : Type) [ring A] (a b c : A) :
a = -b - c + (a + b + c) :=
begin
  ring,
end

[Utensil Song]

Oh I see, tactic#ring is for commutative (semi)rings

[Jalex Stark]

that's why we have tactic#noncomm_ring, which is much more low-tech than tactic#ring

[Jalex Stark]

this works for me

example (A : Type) [ring A] (a b c : A) :
a = -b - c + (a + b + c) := by noncomm_ring

[Utensil Song]

Oh, tatics are named in an opposite way of the type classes, hence the confusion.

[Jalex Stark]

yeah, ring came first

[Jalex Stark]

it's a pretty nontrivial algorithm, there's a paper about the implementation of ring_exp

[Jalex Stark]

but noncomm_ring is a little bit more than a clever simp set

[Utensil Song]

yeah I noticed that paper

[Jalex Stark]

yeah noncomm_ring uses a clever simp set to process the expression into something that abel can handle

[Jalex Stark]

(and then calls abel on it)

[Scott Morrison]

We should possibly add a "front-end" algebra tactic, that inspects the goal and cleverly dispatches to one of ring, noncomm_ring, group, abel, or possibly even linarith and norm_num.

[Scott Morrison]

Possibly it should print a "Try this:" string if we'd prefer people to replace it with a more explicit tactic call.