package coq-aac-tactics

  1. Overview
  2. No Docs
Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators

Install

Dune Dependency

github.com Edit opam file Versions (21)

Authors

  1. T
    Thomas Braibant
  2. D
    Damien Pous
  3. F
    Fabian Kunze

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.14.1.tar.gz
sha512=25112c3321f69423d88356cdf075e7e677cee9629e4f5b06d311cdbc183b810da4f20f12290b28f5e71d0f397b83e71cd03ec50b616277d4db26171a5078f6c5

Description

This Coq plugin provides tactics for rewriting and proving universally quantified equations modulo associativity and commutativity of some operator, with idempotent commutative operators enabling additional simplifications. The tactics can be applied for custom operators by registering the operators and their properties as type class instances. Instances for many commonly used operators, such as for binary integer arithmetic and booleans, are provided with the plugin.

Tags

category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2021-10-10

Published: 17 Oct 2021

Dependencies (2)

  1. coq >= "8.14" & < "8.15~"
  2. ocaml >= "4.05.0"

Dev Dependencies

None

Conflicts

None