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
- Author(s):
- Thomas Braibant (initial)
- Damien Pous (initial)
- Coq-community maintainer(s):
- Tej Chajed (@tchajed)
- License: GNU Lesser General Public License v3.0 or later
- Compatible Coq versions: master (use the corresponding branch or release for other Coq versions)
- Compatible OCaml versions: 4.09.0 or later
- Additional dependencies: none
- Coq namespace:
ATBR
- Related publication(s):
The easiest way to install the latest released version of ATBR is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-atbr
To instead build and install manually, do:
git clone https://github.com/coq-community/atbr.git
cd atbr
make # or make -j <number-of-cores-on-your-machine>
make install
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.
Filename | Description |
---|---|
ATBR | Export all relevant modules, except those related to matrices |
ATBR_Matrices | Export all relevant modules, including those related to matrices |
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 |
SemiLattice | Semilattices, tactics: normalise, reflexivity, rewrite |
SemiRing | Idempotent semirings, tactics: normalise, reflexivity, rewrite |
KleeneAlgebra | Kleene algebras, basic properties |
Converse | Structures with converse (semirings and Kleene Algebras) |
Functors | Functors between the various algebraic structures |
StrictKleeneAlgebra | Class of Strict Kleene algebras (without 0), and extension of the decision procedure |
Filename | Description |
---|---|
Model_Relations | Kleene Algebra of (heterogeneous) binary relations |
Model_StdRelations | Kleene Algebra of standard (homogeneous) binary relations |
Model_Languages | Kleene Algebra of languages |
Model_RegExp | Kleene Algebra of regular expressions (syntactic free model), typed reification |
Model_MinMax | (min,+) Kleene Algebra (matrices on this algebra give weighted graphs) |
Filename | Description |
---|---|
MxGraph | Matrices without operations; blocks definitions |
MxSemiLattice | Semilattices of matrices |
MxSemiRing | Semiring of matrices |
MxKleeneAlgebra | Kleene algebra of matrices (definition of the star operation) |
MxFunctors | Extension of functors to matrices |
Filename | Description |
---|---|
DKA_Definitions | Base definitions for the decision procedure for KA (automata types, notations, ...) |
DKA_StateSetSets | Properties about sets of sets |
DKA_CheckLabels | Algorithm to check whether two regex have the same set of labels |
DKA_Construction | Construction algorithm, and proof of correctness |
DKA_Epsilon | Removal of epsilon transitions, proof of correctness |
DKA_Determinisation | Determinisation algorithm, proof of correctness |
DKA_Merge | Union of DFAs, proof of correctness |
DKA_DFA_Language | Language recognised by a DFA, equivalence with the evaluation of the DFA |
DKA_DFA_Equiv | Equivalence check for DFAs, proof of correctness |
DecideKleeneAlgebra | Kozen's initiality proof, kleene_reflexivity tactic |
Filename | Description |
---|---|
StrictStarForm | Conversion of regular expressions into strict star form, kleene_ssf tactic |
Equivalence | Tactic for solving equivalences by transitivity |
Filename | Description |
---|---|
Examples | Small tutorial file, that goes through our set of tactics |
ChurchRosser | Simple usages of kleene_reflexivity to prove commutation properties |
ChurchRosser_Points | Comparison between a standard CR proof and algebraic ones |
Filename | Description |
---|---|
Common | Shared simple tactics and definitions |
BoolView | View mechanism for Boolean computations |
Numbers | NUM interface, to abstract over the representation of numbers, sets, and maps |
Utils_WF | Utilities about well-founded relations; partial fixpoint operators (powerfix) |
DisjointSets | Efficient implementation of a disjoint sets data structure |
Force | Functional memoisation (in case one needs efficient matrix computations) |
Reification | Reified syntax for the various algebraic structures |
Filename | Description |
---|---|
MyFSets | Efficient ordered datatypes constructions (for FSets functors) |
MyFSetProperties | Handler for FSet properties |
MyFMapProperties | Handler for FMap properties |
Filename | Description |
---|---|
reification.ml |
reification for the reflexive tactics |
Tactic | Description |
---|---|
semiring_reflexivity |
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 |
Tactic | Description |
---|---|
ac_rewrite H |
rewrite a closed equality modulo (AC) of (+) |
monoid_rewrite H |
rewrite a closed equality modulo (A) of (*) |
Tactic | Description |
---|---|
converse_down |
push converses down to terms leaves |
switch |
add converses to the goal and push them down to terms leaves |
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.