This library provides algebraic tools for working with binary relations.
The main tactic provided is a reflexive tactic for solving (in)equations
in an arbitrary Kleene algebra. The decision procedure goes through
standard finite automata constructions.
Note that the initial authors consider this library to be superseded
by the Relation Algebra library, which is based on derivatives
rather than automata: https://github.com/damien-pous/relation-algebra
git clone https://github.com/coq-community/atbr.git
cd atbr
make # or make -j <number-of-cores-on-your-machine>
make install
Documentation
The development and underlying theory of the library is described in the paper
Deciding Kleene Algebras in Coq, Logical Methods in Computer Science,
Volume 8, Issue 1, 2012.
Below are succinct descriptions of each file and tactic. See also the
coqdoc presentation of the Coq source files from the latest release.
Library files
Filename
Description
ATBR
Export all relevant modules, except those related to matrices
ATBR_Matrices
Export all relevant modules, including those related to matrices
Algebraic hierarchy
Filename
Description
Classes
Definitions of algebraic classes of the development
Graph
Lemmas and hints about the base class (carrier with equality)
Monoid
Monoids, free monoids, finite iterations over a monoid, various tactics
solve an (in)equation on the idempotent semiring (*,+,1,0)
semiring_normalize
simplify an (in)equation on the idempotent semiring (*,+,1,0)
semiring_clean
simplify 0 and 1
semiring_cleanassoc
simplify 0 and 1, normalize the parentheses
kleene_reflexivity
solve an (in)equation in Kleene Algebras
ckleene_reflexivity
solve an (in)equation in Kleene Algebras with converse
skleene_reflexivity
solve an (in)equation in Strict Kleene Algebras (without 0)
kleene_clean_zero
remove zeros in a KA expression
kleene_ssf
put KA expressions into strict star form
Rewriting tactics
Tactic
Description
ac_rewrite H
rewrite a closed equality modulo (AC) of (+)
monoid_rewrite H
rewrite a closed equality modulo (A) of (*)
Other tactics
Tactic
Description
converse_down
push converses down to terms leaves
switch
add converses to the goal and push them down to terms leaves
Acknowledgements
The initial authors would like to thank Guilhem Moulin and Sebastien Briais,
who participated to a preliminary version of this project. They are also grateful
to Assia Mahboubi, Matthieu Sozeau, Bruno Barras, and Hugo Herbelin for highly
stimulating discussions, as well as numerous hints for solving various problems.
I'm interested in experimenting with this project using Coq 8.9. However, currently, the master branch does not compile with Coq 8.9beta1 or Coq's v8.9 branch. Any chance for a v8.9 branch I can target with PRs, or can I just create that branch?
The symptom is an error No rule to make target reification.cmxs', needed by Reification.vo'.
Coq no longer builds ml4 files so reification.ml4 has to be ported to coqpp (a reification.mlg file). The OCaml logic there should also be moved to an ordinary ml file.
Alternately, I might just move the reification into Ltac.
The checking time of the project increased from around 7 minutes in Coq 8.10 to around 18 minutes in 8.11+beta1 and master (as measured by Travis). This could be due to changes in omega and deserves further investigation.
Is there a plan to do a release for coq 8.13?
The latest release is compiling with a deprecation warning about Coqlib.find_reference.
The same issue occurs on the coq-8.13-compat branch.
I'm also getting some warnings at link-time. ld complains about not finding any directory for Coq IDE -- both on the latest release and the coq-8.13-compat. Should coq-ide be considered as a dependency of atbr?