Handling associativity when rewriting expressions

Stream: metaprogramming / tactics

[Sam Ezeh]

At a high level I know which expressions I'd like to apply theorems to and I also have the corresponding Expr data but they sometimes might be associated in the wrong way in the goal. So if I have a rule a + b = a' and the expression a + (b + c) I'd like to rewrite this to a' + c. Is there a solution to this?

My specific use case is for composition of morphisms/linear maps. I don't care about the association of the resulting goal but I need to be able to apply a theorem regardless of the association. For morphisms in a category, I'm aware of reassoc_of% and it works fairly well but using it blindly fails on cases such as this

example [Category C] {T : Monad C} : T.map (T.η.app X) ≫ T.μ.app _ = (Monad.η T).app (T.obj X) ≫ (Monad.μ T).app _
  := by
      rw [reassoc_of% T.left_unit] -- fails
      rw [T.left_unit] -- works

I could take the implementation of reassoc_of% and write something similar for composing linear maps but I think it would have the same issue. What I want is a way to go from Expr and a theorem then apply it with these expressions while ignoring associativity.

@Anand Rao Tadipatri have you dealt with this in your graphical rewriter?/Do you have any insight?

[Anand Rao Tadipatri]

No, unfortunately I haven't dealt with rewrites up to associativity or commutativity. This seems tricky to implement.

[Adam Topaz]

You could take a look at how prod_assoc% is implemented and do something similar.

[Adam Topaz]

mathlib(3) also had assoc_rw. Did that ever make it into lean4?

[Kevin Buzzard]

I mentioned rw_assoc in this thread last month but nobody said "yes it's there". By the way @Sam Ezeh I was also thinking about bialgebras and Hopf algebras when I asked that question. Some Imperial undergrads have made a lot of progress with Hopf algebras and their relation to group functors and group schemes.