Damien Pous' home page
Relation Algebra and KAT in Coq
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
- 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
This library is distributed under the terms of the GNU Lesser General
Public License version 3. It is available through opam, under the
. Alternatively, here are the various versions:
The library is also available
and as a Coq contribution
(version 1.3 of the library for the later).
Related papers or talks
- The tactic for KAT and its various applications are described
Kleene Algebra with Tests and Coq Tools for while Programs.
D. Pous, in Proc. ITP'13, LNCS 7998, July 2013.
- A beta version of this library was presented at RAMiCS, September 2012: slides.
- The generalisation to typed structures, and the untyping
theorems are explained in details in
Untyping Typed Algebras and Colouring Cyclic Linear Logic.
D. Pous, Logical Methods in Computer Science, 2012.
- A description of ATBR, the ancestor of this library (see the notes below) appeared in
Deciding Kleene Algebras in Coq.
T. Braibant and D. Pous, Logical Methods in Computer Science,
- We closely follow the work of Dexter Kozen for KA and KAT
- 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:
- Decision tactics:
ka: equational theory of Kleene algebra;
kat: equational theory of Kleene algebra with tests;
hkat: Hoare theory of Kleene algebra with tests:
it exploits hypotheses of the shape
[a]*p == p*[a],
[a]*p == [p], and all similar ones.
lattice: solves lattice (in)equations, using
focused proof search (modular tactic: it works from preorders to
bounded distributed lattices).
- Incomplete decision tactics:
ra: tries to solve relation algebra (in)equations, by
normalisation and comparison. This tactic is modular: it applies
to all algebraic theories present in the library.
hlattice: tries to solve the Horn theory of lattices
- Normalisation tactics:
ra_normalise: normalise the current goal (modular tactic);
ra_simpl: normalise the current goal, without
distributing composition over unions (modular tactic).
- Rewriting tactics:
mrewrite: rewriting modulo associativity of
composition (ad-hoc tactic);
- the library can easily be interfaced with
to obtain more powerful AC rewriting tools (see the
- Other tactics:
lattice.dual: prove goals by lattice duality;
monoid.dual: prove goals by categorical duality;
neg_switch: revert a goal to exploit the Boolean
cnv_switch: revert a goal to exploit the
Succinct description of each module
Each module is documented; links below point to the coqdoc generated
documentation; see below for dependencies.
The coqdoc table of contents is here.
common: basic tactics and definitions used
throughout the library
comparisons: types with decidable equality
and ternary comparison function
positives: simple facts about binary positive numbers
ordinal: finite ordinals, finite sets of
pair: encoding pairs of ordinals as ordinals
powerfix: simple pseudo-fixpoint iterator
lset: sup-semilattice of finite sets represented as lists
- Algebraic hierarchy
level: bitmasks allowing us to refer to an
arbitrary point in the hierarchy
lattice: ``flat'' structures, from preorders
to Boolean lattices
monoid: typed structures, from partially
ordered monoids to residuated Kleene lattices
kat: Kleene algebra with tests
kleene: Basic facts about Kleene algebra
factors: Basic facts about residuated structures
relalg: Standard relation algebra facts and definitions
prop: distributed lattice of Prop-ositions
boolean: Boolean trivial lattice, extended
to a monoid.
rel: heterogeneous binary relations
lang: word languages (untyped)
traces: trace languages (typed and untyped)
glang: guarded string languages (typed and untyped)
- Free models
lsyntax: free lattice (Boolean expressions)
atoms: atoms of the free Boolean lattice over a finite set
syntax: free relation algebra
regex: regular expressions (untyped)
gregex: generalised regular expressions
(typed - for KAT completeness)
ugregex: untyped generalised regular
expressions (for KAT decision procedure)
kat_reification: tools and definitions for
- Relation algebra tools
normalisation: normalisation and
semi-decision tactics for relation algebra
rewriting: rewriting modulo associativity of
composition ; bridge with AAC_tactics (disabled by default)
move: tools to easily move subterms inside a product
- Linear algebra
sups: finite suprema/infima (a la bigop from
sums: finite sums
matrix: matrices over all structures
supporting this construction
matrix_ext: additional operations and
properties about matrices
rmx: matrices of regular expressions
bmx: matrices of Booleans
- Untyping theorems
untyping: untyping theorem for structures
below Kleene algebra with converse
kat_untyping: untyping theorem for guarded
string languages (and thus, KAT)
dfa: deterministic finite state automata,
decidability of language inclusion
nfa: matricial non-deterministic finite
state automata, formal evaluation into regular expressions
ugregex_dec: decision of guarded string
language equivalence of generalised regular expressions, using
ka_completeness: (untyped) completeness of Kleene algebra
kat_completeness: (typed) completeness of Kleene
algebra with tests
kat_tac: decision tactics for KA and KAT,
elimination of Hoare hypotheses to get
- Applications to program verification
compiler_opts: verification of compiler
optimisations in 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.
I am grateful to Thomas Braibant, with whom we developed the ancestor
of this library, clearing the ground for this subsequent work.