Zulip Chat Archive

Stream: Is there code for X?

Topic: add_comm_group tactic?


view this post on Zulip Kevin Buzzard (Jun 13 2020 at 17:48):

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.

view this post on Zulip Johan Commelin (Jun 13 2020 at 17:49):

Doesn't abel do this?

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 17:50):

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

view this post on Zulip Scott Morrison (Jun 13 2020 at 23:25):

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

view this post on Zulip Scott Morrison (Jun 13 2020 at 23:25):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 00:08):

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

view this post on Zulip Utensil Song (Jun 14 2020 at 01:12):

@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

view this post on Zulip Utensil Song (Jun 14 2020 at 01:30):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:32):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:33):

this works for me

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

view this post on Zulip Utensil Song (Jun 14 2020 at 01:35):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:36):

yeah, ring came first

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:37):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:37):

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

view this post on Zulip Utensil Song (Jun 14 2020 at 01:38):

yeah I noticed that paper

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:38):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 01:39):

(and then calls abel on it)

view this post on Zulip Scott Morrison (Jun 14 2020 at 04:05):

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.

view this post on Zulip Scott Morrison (Jun 14 2020 at 04:05):

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


Last updated: May 17 2021 at 16:26 UTC