Coq中模AC推理策略
Tactics for Reasoning modulo AC in Coq
摘要：
我们提出了一套工具，用于重写模结合性和交换性（AC）在Coq，解决了一个长期存在的实际问题。我们使用两个构建块：第一，用于等式模AC的可扩展自反判定过程;第二，用于模式匹配模AC的OCaml插件。我们处理仅关联操作，中性元素，未解释的函数符号和用户定义的等价关系。通过依赖于具体化阶段的类型类，我们可以自动推断这些属性，因此最终用户不需要指定哪个操作是A或AC，或者哪个常量是中性元素。
英文摘要：
We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision procedure for equality modulo AC; second, an OCaml plug-in for pattern matching modulo AC. We handle associative only operations, neutral elements, uninterpreted function symbols, and user-defined equivalence relations. By relying on type-classes for the reification phase, we can infer these properties automatically, so that end-users do not need to specify which operation is A or AC, or which constant is a neutral element.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
