Can [simp] theorems apply "through parentheses"?

Stream: lean4

[Mitchell Lee]

Here's a theorem I have. It states that a simple reflection multiplied by itself gives the identity. (Here, (s i) refers to an element of a particular group.)

@[simp] theorem simple_mul_self (i : B) : (s i) * (s i) = 1

Now, suppose I have an expression like g * (s i) * (s i). The simplifier can't correctly simplify this to g because it's really (g * (s i)) * (s i), so (s i) * (s i) never actually appears anywhere. Is there any way to fix this?

[Matt Diamond]

you can rewrite with docs#mul_assoc

[Mitchell Lee]

What I mean is: is there any way to make the simplifier do it automatically?

[Matt Diamond]

you mean beyond just doing simp [mul_assoc]? like marking mul_assoc as a simp lemma?

[Matt Diamond]

I'm not sure if there's a way to tell Lean "simp should try mul_assoc before simple_mul_self if simple_mul_self doesn't work" without making mul_assoc a simp lemma more generally... but there could be a trick I'm unaware of

[Mitchell Lee]

I think I will just go with adding a separate theorem that says that g * (s i) * (s i) is equal to g, but I was wondering if there was a different solution.

[James Gallicchio]

this is hard to automate in general, and I don't think there's a general-purpose way to get simp to do what you want. if there's more structure here then sometimes you can use stronger (but more specific) automation such as ring or omega, or you can use more bruteforce automation such as aesop which you can instruct to blindly apply associativity/commutativity in its search for proofs. but simp alone is not designed to handle this situation.

[Kyle Miller]

That's probably easiest @Mitchell Lee. Mathlib's category theory library has a @[reassoc] attribute that generates similar lemmas for compositions of morphisms in a category. There could be such a metaprogram for binary operations such as *.

[Kim Morrison]

Mitchell Lee said:

I think I will just go with adding a separate theorem that says that g * (s i) * (s i) is equal to g, but I was wondering if there was a different solution.

This is exactly what @[reassoc] does (but for categorical composition, rather than multiplication).

It works great, as far as it goes. :-)

[Kyle Miller]

Mathlib 3 also had the assoc_rewrite tactic, which I'm not sure I ever used.