I wonder what is the most elegant way of rearranging associative terms in Coq. I think it is a well-defined problem for some existing operators, such as plus.
I have defined new associative operater and operands with corresponding types. In short, an associative lemma states that
Lemma assoc: forall A B C: sometype, A # (B # C) = A # B # C
Surely, all chains organized in the same order are equal no matter how to put the brackets. e.g.
A # B # C # D # E = (A # B) # (C # (D # E)) = (A # (B # (C # (D # E))))
I know one can use repeat rewrite assoc. or repeat rewrite <- assoc.to achieve LHS or RHS from the middle expression. Now I want to apply a lemma about (B # C). How can I quickly rewrite the expression to something like,
A # (B # C) # D # E
One solution is to use replace ... with ... by now rewrite assoc. However, it can be tedious when the expressions are getting longer. Is there any other effective way of rearranging terms/bracket? Is the aac-tactics library helpful for the problem? I cannot find a tutorial for using aac over the customized operators.
Yes AAC-Tactics is the recommended tactic for such problems. It provides an extensible tactic for associative and commutative rewriting. The tutorial is here (https://github.com/coq-community/aac-tactics/blob/master/theories/Tutorial.v).
AAC-Tactics is included in Coq Platform, so you can expect long term support for it.