A Tactic for Rewriting modulo AC in Coq
Thomas Braibant, Damien Pous · 2011
We present a set of tools for rewriting modulo associativity and commutativity in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision proce- dure for equality modulo AC; second, an OCaml Coq plug-in for pattern matching modulo AC. Our decision procedure stems from Barendregt's two level approach, but allows to reason with several A/AC operations at the same time, by working with an arbitrary signature.