A basic group equality

Stream: new members

[Way Yan]

import algebra.hom.group
import tactic

example {G : Type} [group G] (a b : G) : (a * b) ^ 3 = a * b * a * b * a * b := by group

Why doesn't this work? (It doesn't work for powers of 1 or 2 either.)

[Eric Wieser]

Maybe docs#tactic.interactive.group can't handle powers...

[Eric Wieser]

Does the example in the docs that uses ^ work?

[Kyle Miller]

group is implemented using simp, and it doesn't look like it has any lemmas for (a * b) ^ n

[Ruben Van de Velde]

It's weird - this works

example {G : Type*} [group G] (a b : G) : a * (a * b) * b = a ^ 2 * b ^ 2 :=
by group

[Kyle Miller]

That's fine, it's not using powers of the form (a * b) ^ n. It only can handle (a * b) ^ -1, as far as I understand.

[Junyan Xu]

Yeah ⁻¹ docs#has_inv.inv is not a power.

[Way Yan]

Would it be a good idea to add some simp lemmas for (a * b) ^ n then?

[Junyan Xu]

Well for n = 2 we have docs#sq, but it's not clear if either side is simpler than the other, so it's appropriately not marked a simp lemma. For higher n, the product expansion is more complicated, but if you want to expand (for an explicit n) you can always do something like simp only [pow_succ].

[Kyle Miller]

@Junyan Xu The key is that it's for (a * b) ^ n, not just a ^ n, since group seems to be meant to expand and collect powers.

[Damiano Testa]

A different approach would be to expand an expression in a group into a list and simplify from there. This would likely be more stable than calling several simp lemmas, giving more control over what to do.

[Junyan Xu]

Yeah maybe just normalizing the expressions to reduced words? I think there's even a function in mathlib for that (docs#free_group.reduce), so the algorithm is there.

[Kyle Miller]

That's "just" what the simp set for group is trying to do. If it just had some mul_pow_succ lemma it'd work.

So long as simp sets are confluent there's no need to worry about stability.

[Damiano Testa]

Isn't line 73 of docs#tactic.group trying that? Maybe the issue is with parenthesizing.

[Eric Wieser]

That's zpow not pow

[Damiano Testa]

Yes, but I think that a simp call earlier converts nat_pow to int_pow.

[Damiano Testa]

Line 71: symm_expr ``(zpow_coe_nat),

[Damiano Testa]

I think that the heuristic is to convert the exponents to integers, and then simplify the integers via ring.

[Eric Wieser]

try (aux_group₁ locat) looks suspicious to me

[Eric Wieser]

What if that tactic now fails every time due to a lemma rename?

[Damiano Testa]

I also see that the tactic is used very rarely: would it be used more if it were implemented to work in more cases?

[Damiano Testa]

There are some tests: maybe we can make sure that there is a test for each lemma that is used.

[Eric Wieser]

I'm suggesting we just drop the try

[Eric Wieser]

Perhaps replacing it with {fail_if_unchanged := ff} or whatever the spelling is

[Damiano Testa]

I see: I still have to get used to error reporting.

[Damiano Testa]

Without the try this test fails:

example (n : ℤ) (a : G) (h : a^(n*(n+1)-n -n^2) = a) : a = 1 :=
begin
 group at h,
 exact h.symm,
 end

[Damiano Testa]

Let me see if I understand what is going on.

[Damiano Testa]

So, the try seems to be there since you want to preprocess the expression to get rid of fluff. But it does not want to fail if there is not fluff to be cleared.

[Damiano Testa]

This also fails:

example (n : ℤ) (a : G) (h : a ^ n = a ^ n) : a = 1 :=
begin
 group at h,
 exact h.symm,
end

[Kyle Miller]

Damiano Testa said:

Isn't line 73 of docs#tactic.group trying that? Maybe the issue is with parenthesizing.

By the way, docs#zpow_mul is for a ^ (b * c) rather than (a * b) ^ c

[Damiano Testa]

Kyle, so maybe I wanted to give this line:

symm_expr ``(zpow_add),

?

[Kyle Miller]

That one's for a ^ m * a ^ n -> a ^ (m + n), to coalesce exponents. The problem in the original example is that it's not expanding (a * b) ^ 3 to a * b * a * b * a * b

[Kyle Miller]

@[simp] lemma mul_pow_bit0 {G : Type} [monoid G] (a b : G) (n : ℕ) :
  (a * b) ^ (bit0 n) = (a * b) ^ n * (a * b) ^ n := pow_bit0 _ _

@[simp] lemma mul_pow_bit1 {G : Type} [monoid G] (a b : G) (n : ℕ) :
  (a * b) ^ (bit1 n) = (a * b) ^ n * (a * b) ^ n * (a * b) := pow_bit1 _ _

example {G : Type} [group G] (a b : G) : (a * b) ^ 3 = a * b * a * b * a * b := by simp [mul_assoc]

[Kyle Miller]

There's a problem with these, though, in that they can't be in the same simp set as the other lemmas since there's a tension between them. Maybe group should have two simp passes -- an expansion phase to turn everything into a product of powers of non-products, then a coalescing phase to implement word reduction?

[Eric Wieser]

(I made the change I was thinking of in #15835, but indeed it's not really relevant to the problem)

[Damiano Testa]

Eric, since the lemmas are generated via tactic.simp_arg_type.expr, I think that a name change would produce an error at the tactic level, right?

[Eric Wieser]

You're right; the ``(...) syntax would have already caught that error if it existed

[Eric Wieser]

If one of the lemmas became an invalid simp lemma then there'd be a problem I think

[Damiano Testa]

How about a revamping of the tactic as follows: replace the product by a list, with repetitions for exponents. After that, scan the list looking for 1s and consecutive cancelations, iteratively. Finally, produce a proof that the resulting expression matches the original one.

[Damiano Testa]

Eric Wieser said:

If one of the lemmas became an invalid simp lemma then there'd be a problem I think

Yes, I think so: if I erase a letter in ``(<here>) , I get an immediate error. I think that it looks in the environment for the appropriate name.

[Eric Wieser]

Like I said, my comments above (and #15835) were irrelevant to the topic of this thread