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
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
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 models 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
We give a few examples of applications of this library to program
a formalisation of a paper by Dexter Kozen and Maria-Cristina Patron.
showing how to certify compiler optimisations using KAT.
(See their paper,
and the Coq module
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. (See module imp)
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.
(See Angus and Kozen's paper
and the Coq module paterson.)
This library is available through opam, under the name coq-relation-algebra,
as well as on GitHub.
Our decision algorithm for KAT is probably folklore: its uses
the obvious generalisation of the partial derivatives automaton to
KAT regular expressions, together with a standard on-the-fly bisimulation
algorithm. See the following papers for the coalgebraic treatment of
KA and KAT:
challenging equivalence of two flowchart schemes, due to Paterson
imp: formalisation of the IMP programming
language, proving program equivalence using KAT, embedding of
Hoare logic for partial correctness
This library started by a complete rewrite of the ATBR library we
developed with Thomas Braibant. There was two main reasons for not
reusing this code:
The way we designed the algebraic hierarchy in ATBR, using
typeclasses, did not scale to the richer structures we present here (converse,
residuals, allegories), was not modular enough, and did not allow us
to define easily the Boolean lattice of tests needed in KAT. Here we
follow a completely different approach, which seems to scale pretty
well but required restarting from scratch.
The fact that we were proving the (algebraic) completeness of
KA using the efficient algorithm we designed for deciding language
equivalence of regular expressions was sub-optimal: as a consequence
of this choice, our proofs were over-complicated. Instead, by using
a different path here, we prove KA completeness in about 200 lines
of definitions and 200 lines of proofs. This refactorisation was
essential to reach KAT with a reasonable amount of efforts.
Damien Pous (2012-), CNRS - LIP, ENS Lyon (UMR 5668), France
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-)
I am grateful to Thomas Braibant, with whom we developed the ancestor
of this library, clearing the ground for this subsequent work.