coq-community/atbr

Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

ATBR

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

Meta

• 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):
  • Deciding Kleene Algebras in Coq doi:10.2168/LMCS-8(1:16)2012

Building and installation instructions

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

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
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

Models

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)

Matrices

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

Decision procedure for KA

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

Other tools

Filename	Description
StrictStarForm	Conversion of regular expressions into strict star form, kleene_ssf tactic
Equivalence	Tactic for solving equivalences by transitivity

Examples

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

Misc.

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

Finite sets and maps

Filename	Description
MyFSets	Efficient ordered datatypes constructions (for FSets functors)
MyFSetProperties	Handler for FSet properties
MyFMapProperties	Handler for FMap properties

OCaml modules

Filename	Description
reification.ml	reification for the reflexive tactics

Tactics

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

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.

atbr's Issues

Branch for Coq 8.9?

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?

Build is broken on Coq master

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.

Checking time increase in 8.11 and master

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.

Release for coq 8.13

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?

Thanks!

Release for Coq 8.9

@tchajed do you mind if I do a release for Coq 8.9 (to submit to the OPAM archive)? We'd like to have a timestamp on this project.

I can also step up as co-maintainer for the project if that's all right with you.