Relation algebra library for Coq
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.gitattributes git files Jul 27, 2015
.gitignore _CoqProject / coq_makefile build infrastructure Jun 5, 2018
CHANGELOG authors, html page Dec 4, 2018
COPYING fixing license files Mar 7, 2016
COPYING.LESSER fixing license files Mar 7, 2016
LICENSE fixing license files Mar 7, 2016
Makefile opam file with optional dependency for ssreflect Dec 4, 2018
README.md authors, html page Dec 4, 2018
_CoqProject [coq8.10]: port to ocamlpp / fix compilation errors Dec 6, 2018
all.v add all.v exporting everything except examles Dec 3, 2018
atoms.v use unicode symbols for lattice operations Jun 11, 2018
bmx.v
boolean.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
common.v [coq8.10]:explicityly mention core database Dec 7, 2018
comparisons.v Ajout de la contribution RelationAlgebra Jan 9, 2013
compiler_opts.v
denum.v Ajout de la contribution RelationAlgebra Jan 9, 2013
deps.sh release 1.4 for coq 8.5 Feb 9, 2016
description description and webpage Feb 10, 2016
dfa.v use unicode symbols for lattice operations Jun 11, 2018
factors.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
fhrel.v instance for boolean relations on finType Dec 4, 2018
glang.v Ajout de la contribution RelationAlgebra Jan 9, 2013
gregex.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
imp.v [coq8.10]: declare notation scopes Dec 7, 2018
index.html authors, html page Dec 4, 2018
ka_completeness.v change definition of [le_bool a b] to [a -> b] Dec 3, 2018
kat.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
kat_completeness.v resolve name conflict on import Dec 7, 2018
kat_dec.ml Ajout de la contribution RelationAlgebra Jan 9, 2013
kat_dec.mli Ajout de la contribution RelationAlgebra Jan 9, 2013
kat_reification.mlg [coq8.10]: fix last ocaml error Dec 7, 2018
kat_reification.mllib Ajout de la contribution RelationAlgebra Jan 9, 2013
kat_reification.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
kat_tac.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
kat_untyping.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
kleene.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
lang.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
lattice.v [coq8.10]: declare notation scopes Dec 7, 2018
level.v [coq8.10]: declare notation scopes Dec 7, 2018
lset.v
lsyntax.v [coq8.10]: declare notation scopes Dec 7, 2018
matrix.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
matrix_ext.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
monoid.v remove unused coercion Dec 7, 2018
move.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
mrewrite.mlg [coq8.10]: resolve some OCaml deprecation warning Dec 7, 2018
mrewrite.mllib add .mllib files so that the .cmxs files get installed Jun 6, 2018
nfa.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
normalisation.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
opam opam file with optional dependency for ssreflect Dec 4, 2018
ordinal.v [coq8.10]: declare notation scopes Dec 7, 2018
pair.v properly wrap ltb notations in scope Dec 3, 2018
paterson.v rename rel to hrel to avoid clash with rel in MathComp Dec 3, 2018
positives.v Ajout de la contribution RelationAlgebra Jan 9, 2013
powerfix.v Ajout de la contribution RelationAlgebra Jan 9, 2013
prop.v Ajout de la contribution RelationAlgebra Jan 9, 2013
ra.png Ajout de la contribution RelationAlgebra Jan 9, 2013
ra_common.ml
ra_common.mllib add .mllib files so that the .cmxs files get installed Jun 6, 2018
ra_fold.mlg [coq8.10]: port to ocamlpp / fix compilation errors Dec 6, 2018
ra_fold.mllib add .mllib files so that the .cmxs files get installed Jun 6, 2018
ra_reification.mlg [coq8.10]: port to ocamlpp / fix compilation errors Dec 6, 2018
ra_reification.mllib add .mllib files so that the .cmxs files get installed Jun 6, 2018
regex.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
rel.v heterogeneous relations in Type (rather than Set) Dec 4, 2018
relalg.v [coq8.10]: work around coq issue #8819 Dec 7, 2018
rewriting.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
rmx.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
sums.v replace << with ≪ to avoid clash with << _ >> from MathComp Dec 3, 2018
sups.v heterogeneous relations in Type (rather than Set) Dec 4, 2018
syntax.v
traces.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
ugregex.v heterogeneous relations in Type (rather than Set) Dec 4, 2018
ugregex_dec.v use ⋅ for "dot" operation, rather than * Dec 3, 2018
untyping.v

README.md

Relation Algebra for Coq

Webpage of the project: http://perso.ens-lyon.fr/damien.pous/ra

DESCRIPTION

This Coq development is a modular library about relation algebra: those algebras admitting heterogeneous binary relations as a model, ranging from partially ordered monoid to residuated Kleene allegories and Kleene algebra with tests (KAT).

This library presents this large family of algebraic theories in a modular way; it includes several high-level reflexive tactics:

  • [kat], which decides the (in)equational theory of KAT;
  • [hkat], which decides the Hoare (in)equational theory of KAT (i.e., KAT with Hoare hypotheses);
  • [ka], which decides the (in)equational theory of KA;
  • [ra], a normalisation based partial decision procedure for Relation algebra;
  • [ra_normalise], the underlying normalisation tactic.

The tactic for Kleene algebra with tests is obtained by reflection, using a simple bisimulation-based algorithm working on the appropriate automaton of partial derivatives, for the generalised regular expressions corresponding to KAT.

Combined with a formalisation of KA completeness, and then of KAT completeness on top of it, this provides entirely axiom-free decision procedures for all model of these theories (including relations, languages, traces, min-max and max-plus algebras, etc...).

Algebraic structures are generalised in a categorical way: composition is typed like in categories, allowing us to reach "heterogeneous" models like rectangular matrices or heterogeneous binary relations, where most operations are partial. We exploit untyping theorems to avoid polluting decision algorithms with these additional typing constraints.

APPLICATIONS

We give a few examples of applications of this library to program verification:

  • a formalisation of a paper by Dexter Kozen and Maria-Cristina Patron. showing how to certify compiler optimisations using KAT.
  • a formalisation of the IMP programming language, followed by: 1/ some simple program equivalences that become straightforward to prove using our tactics; 2/ a formalisation of Hoare logic rules for partial correctness in the above language: all rules except the assignation one are proved by a single call to the hkat tactic.
  • a proof of the equivalence of two flowchart schemes, due to Paterson. The informal paper proof takes one page; Allegra Angus and Dexter Kozen gave a six pages long proof using KAT; our Coq proof is about 100 lines.

INSTALLATION

Run 'make' to compile the library, and 'make install' to install it. Latest version compiles with Coq 8.8.2

DOCUMENTATION

Each module is documented, see index.html or http://perso.ens-lyon.fr/damien.pous/ra for:

  • a description of each module's role and dependencies
  • a list of the available user-end tactics
  • the coqdoc generated documentation.

LICENSE

This library is distributed under the terms of the GNU Lesser General Public License version 3. See files LICENSE and COPYING.

AUTHORS

  • Main author

    • Damien Pous (2012-), CNRS - LIP, ENS Lyon (UMR 5668), France
  • Additional authors

    • Christian Doczkal (2018-), CNRS - LIP, ENS Lyon (UMR 5668), France
    • Insa Stucke (2015-2016), Dpt of CS, University of Kiel, Germany
    • Coq development team (2013-)