| Library files: |
| ATBR | Export all relevant modules, except those related to matrices |
| ATBR_Matrices | Export all relevant modules, including those related to matrices |
| Algebraic hierarchy: |
| Classes | Definitions of all 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) |
| Models: |
| Model_Relations | Kleene Algebra of heterogeneous binary relations |
| Model_StdRelations | Kleene Algebra of homogeneous binary relations, from the standard library |
| Model_Languages | Kleene Algebra of languages (initial model) |
| Model_RegExp | Kleene Algebra of regular expression (syntactic free model, include typed reification) |
| Model_MinPlus | (min,+) Kleene Algebra (matrices on this algebra give weighted graphs) |
| Matrices: |
| 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: |
| 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 |
| Examples: |
| 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.: |
| 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) |
| StrictStarForm | Conversion of regular expression into strict star form |
| DisjointSets | Efficient implementation of a disjoint sets data structure |
| Force | Functional memoization |
| Reification | Reified syntax for the various algebraic structures |
| Finite sets and maps: |
| MyFSets.v | Efficient ordered datatypes constructions (for FSets functors) |
| MyFSetProperties.v | Handler for FSet properties |
| MyFMapProperties.v | Handler for FMap properties |
| OCaml modules: |
| Reification | reification for the reflexive tactics |
| Reflexive tactics: |
| 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 |
| kleene_clean_zero | remove zeros in a KA expression |
| kleene_ssf | put KA expressions into strict star form |
| Rewriting tactics: |
| ac_rewrite H | rewrite a closed equality modulo (AC) of (+) |
| monoid_rewrite H | rewrite a closed equality modulo (A) of (*) |
| Other tactics: |
| converse_down | push converses down to terms leaves |
| switch | add converses to the goal and push them down to terms leaves |