如何在Coq中重新排列新定义的关联术语？

问：

我想知道在 Coq 中重新排列联想术语的最优雅方式是什么。我认为对于一些现有的运营商来说，这是一个定义明确的问题，例如 plus。

我已经定义了新的关联运算符和具有相应类型的操作数。简而言之，关联引理指出

Lemma assoc: forall A B C: sometype, A # (B # C) = A # B # C

当然，无论如何放置括号，所有以相同顺序组织的链都是相等的。例如

A # B # C # D # E = (A # B) # (C # (D # E)) = (A # (B # (C # (D # E))))

我知道可以从中间表达式使用或实现 LHS 或 RHS。现在我想应用一个关于 的引理。我怎样才能快速将表达式重写为类似的东西，repeat rewrite assoc.repeat rewrite <- assoc.(B # C)

A # (B # C) # D # E

一种解决方案是使用 但是，当表达式越来越长时，它可能会很乏味。有没有其他有效的方法可以重新排列术语/括号？该库对该问题有帮助吗？我找不到使用自定义运算符的教程。replace ... with ... by now rewrite assoc.aac-tacticsaac