Tactics for Reasoning Modulo AC in Coq

DOI10.1007/978-3-642-25379-9_14MaRDI QIDQ3100211zbMATHOpenAlexFDO

Authors Thomas Braibant, Damien Pous

Publication date 22 November 2011

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1106.4448

Mathematics Subject Classification ID

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.

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

• scientific article; zbMATH DE number 3748393 (Why is no real title available?)
• scientific article; zbMATH DE number 2043522 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• An efficient Coq tactic for deciding Kleene algebras
• Complete Sets of Reductions for Some Equational Theories
• Equational reasoning in Isabelle
• 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
• Rewriting Techniques and Applications
• Single elementary associative-commutative matching
• Theorem Proving in Higher Order Logics
• Unification in Boolean rings and Abelian groups

Cited in

(8)

• External rewriting for skeptical proof assistants
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• Extensible and efficient automation through reflective tactics
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Towards Rewriting in Coq
• Types for Proofs and Programs
• Incorporating quotation and evaluation into Church's type theory
• Modeling Permutations in Coq for Coccinelle

Describes a project that uses

Uses Software

• Coq
• Maude
• OCaml
• HOL90

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)