add_comm_group tactic

Stream: maths

[Patrick Massot]

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]

it's on the todo list

[Patrick Massot]

(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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

any non-unital ring satisfies this criterion

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

...at least it's type correct

[Johan Commelin]

Unfortunately, add_comm_group is not the same as module \Z

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

I can't use the depth parameter

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

it complains e is not a function

[Patrick Massot]

so yes, a delimiter may help

[Mario Carneiro]

I'm open to suggestions

[Mario Carneiro]

would rcases_hint e : 4 be too weird?

[Patrick Massot]

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

[Patrick Massot]

so I would say it's fine

[Patrick Massot]

What about trying to guess better names?

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

the depth thing should be fixed

[Patrick Massot]

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]

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?

[Patrick Massot]

No problem, go ahead