Tactics for Reasoning Modulo AC in Coq
From MaRDI portal
Publication:3100211
DOI10.1007/978-3-642-25379-9_14zbMATH Open1350.68227arXiv1106.4448OpenAlexW2096639003MaRDI QIDQ3100211FDOQ3100211
Authors: Thomas Braibant, Damien Pous 
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1106.4448
Recommendations
- Coq Modulo Theory
- An efficient Coq tactic for deciding Kleene algebras
- Proof by computation in the Coq system
- Coq without type casts: a complete proof of Coq Modulo Theory
- Interacting with Modal Logics in the Coq Proof Assistant
- Strict coherence of conditional rewriting modulo axioms
- Modular dependent induction in Coq, Mendler-style
- Modular SMT proofs for fast reflexive checking inside Coq
- A Coq tactic for equality learning in linear arithmetic
- Embedding Deduction Modulo into a Prover
Cites Work
- Equational reasoning in Isabelle
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Complete Sets of Reductions for Some Equational Theories
- Rewriting Techniques and Applications
- Theorem Proving in Higher Order Logics
- Unification in Boolean rings and Abelian groups
- An efficient Coq tactic for deciding Kleene algebras
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Single elementary associative-commutative matching
- External rewriting for skeptical proof assistants
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- First-Class Type Classes
- How to make ad hoc proof automation less ad hoc
Cited In (8)
- Towards Rewriting in Coq
- Extensible and Efficient Automation Through Reflective Tactics
- Types for Proofs and Programs
- Incorporating quotation and evaluation into Church's type theory
- Modeling Permutations in Coq for Coccinelle
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- External rewriting for skeptical proof assistants
Uses Software
This page was built for publication: Tactics for Reasoning Modulo AC in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100211)
