Stream: maths

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

Mario Carneiro (Aug 08 2018 at 17:10):

it's on the todo list

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)

Kevin Buzzard (Aug 08 2018 at 17:13):

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

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.

Mario Carneiro (Aug 08 2018 at 17:13):

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

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

Mario Carneiro (Aug 08 2018 at 17:15):

any non-unital ring satisfies this criterion

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

Patrick Massot (Aug 08 2018 at 17:18):

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

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

Mario Carneiro (Aug 08 2018 at 17:18):

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

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

Mario Carneiro (Aug 08 2018 at 17:20):

...at least it's type correct

Johan Commelin (Aug 08 2018 at 17:32):

Unfortunately, add_comm_group is not the same as module \Z

Mario Carneiro (Aug 08 2018 at 17:34):

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

Mario Carneiro (Aug 08 2018 at 17:35):

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

Patrick Massot (Aug 08 2018 at 18:07):

I can't use the depth parameter

Mario Carneiro (Aug 08 2018 at 18:08):

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

Mario Carneiro (Aug 08 2018 at 18:08):

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

Patrick Massot (Aug 08 2018 at 18:08):

it complains e is not a function

Patrick Massot (Aug 08 2018 at 18:09):

so yes, a delimiter may help

Mario Carneiro (Aug 08 2018 at 18:09):

I'm open to suggestions

Mario Carneiro (Aug 08 2018 at 18:11):

would rcases_hint e : 4 be too weird?

Patrick Massot (Aug 08 2018 at 18:11):

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

Patrick Massot (Aug 08 2018 at 18:11):

so I would say it's fine

Patrick Massot (Aug 08 2018 at 18:17):

What about trying to guess better names?

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:

Mario Carneiro (Aug 08 2018 at 18:40):

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

Mario Carneiro (Aug 08 2018 at 18:41):

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

Mario Carneiro (Aug 08 2018 at 18:41):

the depth thing should be fixed

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!

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 $\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?