Tactics for Reasoning modulo AC in Coq

TL;DR

This paper introduces a comprehensive set of tools for efficient rewriting modulo associativity and commutativity (AC) in Coq, combining decision procedures and pattern matching to automate reasoning tasks.

Contribution

It presents an extensible framework with automatic inference of properties, addressing a long-standing practical challenge in Coq for reasoning modulo AC.

Findings

Successfully handles associative-only operations and neutral elements

Automates property inference using type-classes

Integrates decision procedures with pattern matching for AC reasoning

Abstract

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.