Group Theory Tactic

Stream: new members

[Thomas Browning]

Is there any sort of tactic for group theory? Such a tactic should be able to prove things like the Hall-Witt identity.

[Jalex Stark]

https://en.wikipedia.org/wiki/Hall%27s_identity

[Jalex Stark]

This? I don't understand the [x,y,z] notation, though I understand $x^y$ means $yxy^{-1}$

[Jalex Stark]

for commutative groups (well, commutative groups that happen to be written additively) we have abel

[Jalex Stark]

You can get some of the way to a general group tactic with a well chosen simp set

[Jalex Stark]

If I had a precise statement of this hall's identity i could look for a proof that leverages automation

[Thomas Browning]

[x,y,z] means [[x,y],z] where [x,y]=x y x^{-1} y^{-1}, but that's not super relevant (I'm not specifically interested in the Hall-Witt identity). What I'm getting at is that it is easy to check whether two words in group theory are equal and it seems like there should be a tactic for this

[Jalex Stark]

well, no, it's undecidable in general to check whether are equal?

[Jalex Stark]

i guess you're asking specifically about deciding the word problem for free groups?

[Thomas Browning]

that's right

[Jalex Stark]

(The first step to writing a tactic may be to collect test cases)

[Jalex Stark]

is there a paper describing an algorithm for deciding the word problem for free groups?

[Jalex Stark]

https://rjlipton.wordpress.com/2009/04/16/the-word-problem-for-free-groups/

[Thomas Browning]

I mean, the algorithm is to distribution any inverses (i.e. (gh)^{-1} = h^{-1} g^{-1}), collect powers like g^m and g^n into g^(m+n), and check whether the resulting words are the same

[Thomas Browning]

it's not terribly sophisticated

[Jalex Stark]

(we don't already have it, I'm trying to have a discussion that's explicit enough to start making progress on writing it)

[Thomas Browning]

sure

[Jalex Stark]

i think simp can do what you suggest

[Thomas Browning]

the worry I'm having is associativity

[Jalex Stark]

have you tried any examples?

[Jalex Stark]

trying an example will make a lot more progress than talking at this point

[Thomas Browning]

ok

[Thomas Browning]

give me a minute

[Thomas Browning]

lemma example1 {G} [group G] (g h : G) : (g * h) * (g * h) * g = g * (h * g) * (h * g) := begin sorry, end

[Thomas Browning]

not sure how to add code in zulip

[Thomas Browning]

but simp can't even do that

[Thomas Browning]

although that particular one can be done with repeating mul_assoc

[Thomas Browning]

lemma example1 {G} [group G] (g h : G) : (g * h) * (g * h) * g = g * (h * g) * (h * g) :=
begin
repeat {rw mul_assoc},--if there is no cancellation then this is enough
end

lemma example2 {G} [group G] (g h k : G) : (h * g) * (g⁻¹ * k) = h * k :=
begin
repeat {rw mul_assoc},--if the cancellation is in the middle then you're in trouble
sorry,
end

[Bryan Gin-ge Chen]

We have a related open issue on this here: #2729, see particularly the zulip thread linked from there.

[Reid Barton]

You just need a simp lemma that says g * (g⁻¹ * k) = k

[Kevin Buzzard]

And one for g-1 * (g * k)

[Kevin Buzzard]

There was a thread about the one relator problem recently

[Bryan Gin-ge Chen]

It should be linked in the issue I linked above.

[Bryan Gin-ge Chen]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60group.60.20tactic

[Thomas Browning]

those two simp lemmas don't seem to be enough

@[simp] lemma useful_lemma {G} [group G] (g h : G) : g * (g⁻¹ * h) = h :=
begin
simp,
end

@[simp] lemma useful_lemma_2 {G} [group G] (g h : G) : g⁻¹ * (g * h) = h :=
begin
simp,
end

example {G : Type} [group G] (a b c d : G) : c *(a*b)*(b⁻¹*a⁻¹)*c = c*c :=
begin
simp,
sorry,
end

[Thomas Browning]

However, the group tactic in that thread might be what I need

[Jalex Stark]

(I just give an easier-for-human-to-parse definition of the group tactic from that thread)

meta def nonabel := `[simp only [mul_inv_self, mul_assoc, mul_inv_self, mul_inv_rev,inv_inv,inv_mul_self,mul_inv_cancel_right,mul_inv_cancel_left,inv_mul_cancel_right,inv_mul_cancel_left]]

lemma example1 {G} [group G] (g h : G) :
(g * h) * (g * h) * g = g * (h * g) * (h * g) :=
by nonabel


lemma example2 {G} [group G] (g h k : G) :
(h * g) * (g⁻¹ * k) = h * k :=
by nonabel

[Jalex Stark]

I guess the PR hasn't been made yet

[Jalex Stark]

seems to me like we should put this naive group tactic in mathlib and wait for someone who gets frustrated with it to implement a more efficient / expressive version

[Bryan Gin-ge Chen]

It's not exactly the same since I think Patrick's tactic allows writing group at h.

[Jalex Stark]

ah okay, i thought there must be a reason for the extra complexity but didn't think hard about it

[Jalex Stark]

I guess a PR "just" needs to add a "good enough" set of test cases

[Jalex Stark]

is it plausible to prove a theorem like "if this equation is true in the free group, then this tactic will eventually halt with a proof"?

[Bryan Gin-ge Chen]

Probably not, since tactics live in meta.

[Thomas Browning]

Good news: that group theory tactic can do the Hall-Witt identity!

import tactic

namespace tactic.interactive
setup_tactic_parser
open tactic.simp_arg_type

meta def group (locat : parse location) : tactic unit :=
simp_core {} skip tt [
  expr ``(mul_inv_self),
  symm_expr ``(mul_assoc),
  expr ``(mul_inv_self),
  expr ``(mul_inv_rev),
  expr ``(inv_inv),
  expr ``(inv_mul_self),
  expr ``(mul_inv_cancel_right),
  expr ``(mul_inv_cancel_left),
  expr ``(inv_mul_cancel_right),
  expr ``(inv_mul_cancel_left)]
  [] locat
end tactic.interactive

def commutator {G} [group G] : G → (G → G) := λ g h, g * h * g⁻¹ * h⁻¹

def commutator3 {G} [group G] : G → (G → (G → G)) := λ g h k, commutator (commutator g h) k

example {G} [group G] (g h k : G) : g * (commutator3 g⁻¹ h k) * g⁻¹ * k * (commutator3 k⁻¹ g h) * k⁻¹ * h * (commutator3 h⁻¹ k g) * h⁻¹ = 1 :=
begin
repeat {unfold commutator3},
repeat {unfold commutator},
group,
end

[Jalex Stark]

it would make a nice test case in the PR :)

[Kevin Buzzard]

That's really nice!

Mario was moaning the other day that us mathematicians don't specify our tactics well enough. Perhaps I should keep track better whenever I run into a goal which I feel should be solvable with automation but which I can't solve in Lean without some pain. A collection of tests might be what one needs to make a start at a tactic.

[Jalex Stark]

I intend to collect such observations on the metaprogramming stream

[Mario Carneiro]

there is a metaprogramming stream?

[Jalex Stark]

It's not active (yet?), I made it so that there would be a natural place to collect these "tactic specifications"
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/stream.20events/near/197849636

[Jalex Stark]

most of the content there is a discussion about streams, some which bubbled back up into meta

[Mario Carneiro]

I think that creating new streams is problematic because of lack of discoverability. It's a great way to have conversations that most people won't notice

[Jalex Stark]

yes, i did honestly intend to have conversations that most people won't pay attention to

[Jalex Stark]

once a "tactic specification"is complete enough to deserve attention one could advertise it elsewhere

[Jalex Stark]

maybe I'm just trying to implement a poor version of having a mathlib branch without a PR

[Mario Carneiro]

I think that conversations on general have an appropriate level of exposure for this sort of thing

[Jalex Stark]

thanks, that is a useful judgement

[Mario Carneiro]

conversations on a new non-default public stream are barely better than a group PM

[Jalex Stark]

I agree with that

[Mario Carneiro]

(I see now that the only conversation that has happened so far on the metaprogramming stream is a replay of what I just said)

[Jalex Stark]

I think the following text should be a PR. (I'm trying to make it but this requires me to understand more things about git first)

/-
Copyright (c) 2020. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot, Thomas Browning
-/
import tactic

/-!
# `group`

Evaluate expressions in the language of groups. Ideally this would implement a full algorithm for the word problem in free groups.

## Tags

group_theory
-/

namespace tactic.interactive
setup_tactic_parser
open tactic.simp_arg_type

meta def group (locat : parse location) : tactic unit :=
simp_core {} skip tt [
  expr ``(mul_inv_self),
  symm_expr ``(mul_assoc),
  expr ``(mul_inv_self),
  expr ``(mul_inv_rev),
  expr ``(inv_inv),
  expr ``(inv_mul_self),
  expr ``(mul_inv_cancel_right),
  expr ``(mul_inv_cancel_left),
  expr ``(inv_mul_cancel_right),
  expr ``(inv_mul_cancel_left)]
  [] locat
end tactic.interactive

example {G : Type} [group G] (a b c d : G) : c *(a*b)*(b⁻¹*a⁻¹)*c = c*c :=
by group

example {G : Type} [group G] (a b c d : G) : (b*c⁻¹)*c *(a*b)*(b⁻¹*a⁻¹)*c = b*c :=
by group

example {G : Type} [group G] (a b c d : G) : c⁻¹*(b*c⁻¹)*c *(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 :=
by group


def commutator {G} [group G] : G → (G → G) := λ g h, g * h * g⁻¹ * h⁻¹

def commutator3 {G} [group G] : G → (G → (G → G)) := λ g h k, commutator (commutator g h) k

-- The following is known as the Hall-Witt identity, see e.g. https://en.wikipedia.org/wiki/Three_subgroups_lemma#Proof_and_the_Hall%E2%80%93Witt_identity
example {G} [group G] (g h k : G) : g * (commutator3 g⁻¹ h k) * g⁻¹ * k * (commutator3 k⁻¹ g h) * k⁻¹ * h * (commutator3 h⁻¹ k g) * h⁻¹ = 1 :=
begin
repeat {unfold commutator3},
repeat {unfold commutator},
group,
end

-- todo : a nontrivial example of using `group at h`

[Bryan Gin-ge Chen]

You'll want to add docstrings to all the defs and all the examples should be in test/group.lean. The Hall-Witt identity probably should be in the appropriate group_theory or algebra file. Also don't forget the PR name should follow our commit convention. I just noticed that that file wasn't linked on our website, so I'll fix that.

[Jalex Stark]

thanks, somehow it did not occur to me that there would be a PR naming convention

[Jalex Stark]

i'll try reading a bunch of PRs and see if I notice any other patterns

[Scott Morrison]

Also, you should have a test for the group at h usage.

[Patrick Massot]

I think it doesn't make sense to PR such a broken tactic. I'll try to find time to work on it.

[Patrick Massot]

I think I'm back on track with this tactic. But of course I didn't want to spend time on it today. So anyone who wants to have this tactic really soon is welcome to turn the code at https://gist.github.com/PatrickMassot/051ecff8c84a4a2fcb5c9caf00b65826 into a PR. It means dispatching the lemmas to the right places (maybe all of them should go to algebra.group_power), moving all test into a separate file in the test folder, adding more tests, finding bugs etc. I guess the previous version was faster on the very limited examples that worked, but I hope that one is not too far away from actually doing the job.

[Alex J. Best]

Nice, sorry its hard to read all the lemma, does it work when you have a gpow mul a pow?

[Patrick Massot]

#mwe?

[Patrick Massot]

I forgot to write as part of the PRing process: give actual names to things like gpow_trick_one...

[Alex J. Best]

Looks good!

[Patrick Massot]

Ok, don't hesitate to play more with this. I didn't follow rigorous process here, I mostly randomly added lemmas to the simp set.

[Patrick Massot]

Actually there are edge cases where we should start with ring, so I modified the gist. It now calls ring twice in a row in some edge cases, but I should really stop now

[tsuki hao]

May I ask what package should I import if I want to introduce tactic related to group theory? I tried Mathlib.Group.Basic and got error

[Scott Morrison]

@tsuki hao, I can't work out what you're asking. Is there a particular tactic you have in mind that you are trying to find, or are you asking what group theory relevant tactics are available?

[tsuki hao]

Scott Morrison said:

tsuki hao, I can't work out what you're asking. Is there a particular tactic you have in mind that you are trying to find, or are you asking what group theory relevant tactics are available?

image.jpg
I want to formalize this proof, but I don't know where to find the tactic about groups

[Scott Morrison]

How about you write a Lean proof without any tactics first, and then ask if there are any tactics that would be helpful. (I don't think there is anything specifically about groups that would be useful here.)

[tsuki hao]

Scott Morrison said:

How about you write a Lean proof without any tactics first, and then ask if there are any tactics that would be helpful. (I don't think there is anything specifically about groups that would be useful here.)

Ok, thank you! I'll try it

[tsuki hao]

Does anyone know how to define subgroups formally

[Kevin Buzzard]

Lean already has subgroups. They're Subgroup G

[Bulhwi Cha]

See docs#Subgroup.

[Scott Morrison]

@tsuki hao, my internal method of answering questions of this form is to have a cloned copy of mathlib4 open in VSCode, and to use the search tool to look for e.g. subgroup. You can also search for things on the docs page that Bulhwi just linked to.