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 highlevel reflexive tactics:

The tactic for Kleene algebra with tests is obtained by reflection, using a simple bisimulationbased 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 axiomfree decision procedures for all models of these theories (including relations, languages, traces, minmax and maxplus 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.
We give a few examples of applications of this library to program verification:
compiler_opts
.)
hkat
tactic. (See module imp
)
paterson
.)
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 p==0
,
[a]==[b]
, [a]*p == p*[a]
, [a]*p ==
[p]
, [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).
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
(modular tactic)
ra_normalise
: normalise the current goal (modular tactic);
ra_simpl
: normalise the current goal, without
distributing composition over unions (modular tactic).
mrewrite
: rewriting modulo associativity of
composition (adhoc tactic);
AAC_tactics
,
to obtain more powerful AC rewriting tools (see the
rewriting
) module).
lattice.dual
: prove goals by lattice duality;
monoid.dual
: prove goals by categorical duality;
neg_switch
: revert a goal to exploit the Boolean
negation involution;
cnv_switch
: revert a goal to exploit the
converse involution.
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
finite ordinals
pair
: encoding pairs of ordinals as ordinals
powerfix
: simple pseudofixpoint iterator
lset
: supsemilattice of finite sets represented as lists
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
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
KAT reification
normalisation
: normalisation and
semidecision 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
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 nondeterministic finite
state automata, formal evaluation into regular expressions
ugregex_dec
: decision of guarded string
language equivalence of generalised regular expressions, using
partial derivatives
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 hkat
compiler_opts
: verification of compiler
optimisations in KAT
paterson
:
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: