# Zulip Chat Archive

## Stream: maths

### Topic: add_comm_group tactic

#### 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?

#### Patrick Massot (Aug 08 2018 at 21:38):

No problem, go ahead

Last updated: May 11 2021 at 17:39 UTC