Zulip Chat Archive

Stream: maths

Topic: add_comm_group tactic


view this post on Zulip Patrick Massot (Aug 08 2018 at 17:09):

Could we get a scaled down ring tactic handling add_comm_group? My current goal is φ (x', y') - φ (x, y) = φ (x', y₁) - φ (x, y₁) + (φ (x', y') - φ (x', y₁) - (φ (x, y') - φ (x, y₁))) + (φ (x₁, y') - φ (x₁, y)) + (φ (x, y') - φ (x, y) - (φ (x₁, y') - φ (x₁, y))) and I can't face proving it by hand

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:10):

it's on the todo list

view this post on Zulip Patrick Massot (Aug 08 2018 at 17:10):

(this is a generalization of the thing I called a ring bug the other day because I forgot to tell Lean rings are commutative)

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:13):

Why not put a ring structure on your group? ;-)

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:13):

I think once someone showed me a group for which they could prove that this could not be done, unfortunately.

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:13):

I think I know how to do modules; maybe you could use that

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:14):

Oh yeah, Q/Z. No possibility for 1 because it would be killed by some n, but not everything is killed by n

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:15):

any non-unital ring satisfies this criterion

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:17):

oh, actually I think you stand to gain just a bit by using a module tactic to solve abelian group problems

view this post on Zulip Patrick Massot (Aug 08 2018 at 17:18):

It makes me think I should try the rcases_hint tactic now that you pushed it

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:18):

since it would be able to handle (m * n) . x = m . (n . x) where m,n : Z

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:18):

but a standard abelian group tactic can't deal with Z variables

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:19):

You should definitely try rcases_hint. I wrote 200 lines of lean in one sitting and tested it once at the end, and it seemed to work

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:20):

...at least it's type correct

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:32):

Unfortunately, add_comm_group is not the same as module \Z

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:34):

that's not a significant problem for a tactic, it can supply the instance when needed

view this post on Zulip Mario Carneiro (Aug 08 2018 at 17:35):

speaking of which, someone should prove that instance. All the hard work is already done

view this post on Zulip Patrick Massot (Aug 08 2018 at 18:07):

I can't use the depth parameter

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:08):

The syntax is rcases_hint e {depth := 4} or rintro_hint {depth := 4}

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:08):

the lack of delimiter between e and the cfg may cause a problem

view this post on Zulip Patrick Massot (Aug 08 2018 at 18:08):

it complains e is not a function

view this post on Zulip Patrick Massot (Aug 08 2018 at 18:09):

so yes, a delimiter may help

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:09):

I'm open to suggestions

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:11):

would rcases_hint e : 4 be too weird?

view this post on Zulip Patrick Massot (Aug 08 2018 at 18:11):

it's not meant to stay in the final Lean file anyway

view this post on Zulip Patrick Massot (Aug 08 2018 at 18:11):

so I would say it's fine

view this post on Zulip Patrick Massot (Aug 08 2018 at 18:17):

What about trying to guess better names?

view this post on Zulip Johan Commelin (Aug 08 2018 at 18:34):

speaking of which, someone should prove that instance. All the hard work is already done

Do we want an actual instance, or just 2 lemmas that convert either way. I think we can't have instances both ways, right? That would blow up the type class system :boom:

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:40):

We already have an instance one way, the other one should just be a def

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:41):

I changed rcases_hint to rcases?, hint takes too long to write

view this post on Zulip Mario Carneiro (Aug 08 2018 at 18:41):

the depth thing should be fixed

view this post on Zulip Patrick Massot (Aug 08 2018 at 20:38):

My current goal is φ (x', y') - φ (x, y) = φ (x', y₁) - φ (x, y₁) + (φ (x', y') - φ (x', y₁) - (φ (x, y') - φ (x, y₁))) + (φ (x₁, y') - φ (x₁, y)) + (φ (x, y') - φ (x, y) - (φ (x₁, y') - φ (x₁, y))) and I can't face proving it by hand

This was the last missing piece, so I decided to try it. After about 15 minutes of misery, I found out that apply eq_of_sub_eq_zero, simp does the trick!

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 21:35):

Unfortunately, add_comm_group is not the same as module \Z

OK so in the perfectoid mathlib pile-up there is quotient_group.lean, which I wrote based on quotient_module.lean. But what I actually want is quotient_add_group.lean so I can use it to improve quotient_ring.lean. I see three possibilities for making quotient_add_group.lean :

(1) just copy quotient_group.lean changing all the *s to +s etc.

(2) Some sort of tactic magic

(3) deduce the results from quotient_module.lean using the fact that, as we mathematicians say, an abelian group "is" a Z\mathbb{Z}-module.

Which is the best idea?

@Patrick Massot Do you mind if I put our names on the top of quotient_group.lean (remember -- I wrote it, basically copying from quotient_module.lean and then you fixed up a bunch of stuff and made it better) and PR it to mathlib via the community mathlib?

view this post on Zulip Patrick Massot (Aug 08 2018 at 21:38):

No problem, go ahead


Last updated: May 11 2021 at 17:39 UTC