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 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 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 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. (See their paper, and the Coq module compiler_opts.)
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.)

Download

This library is available through opam, under the name coq-relation-algebra, as well as on GitHub.

Related papers or talks

The tactic for KAT and its various applications are described in
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, 2012.
We closely follow the work of Dexter Kozen for KA and KAT completeness proofs:
- A completeness theorem for Kleene algebras and the algebra of regular events. D. Kozen. Information and Computation, 110(2):366-390, May 1994.
- Kleene algebra with tests: Completeness and decidability. D. Kozen and F. Smith. In Proc. CSL'96, vol. 1258 of LNCS, pages 244-259, 1996. Springer-Verlag.
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:
- Automata and coinduction (an exercise in coalgebra). J. Rutten. In Proc CONCUR '98, LNCS 1466, Springer, 1998, pp. 194-218.
- On the coalgebraic theory of Kleene algebra with tests. D. Kozen. Technical Report, Computing and Information Science, Cornell University, March 2008.

Documentation

Provided tactics

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 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).
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 (modular tactic)
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); more AC rewriting tools are available using the AAC_tactics library.
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 negation involution;
- cnv_switch: revert a goal to exploit the converse involution.

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.

Utilities
- 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 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
Models
- prop: distributed lattice of Prop-ositions
- boolean: Boolean trivial lattice, extended to a monoid.
- rel: heterogeneous binary relations
- srel: heterogeneous binary relations over setoids
- fhrel: heterogeneous binary relations over finite types (requires ssreflect)
- 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 KAT reification
Relation algebra tools
- normalisation: normalisation and semi-decision tactics for relation algebra
- rewriting: rewriting modulo associativity of composition
- rewriting_aac: bridge with AAC_tactics (requires AAC_tactics)
- move: tools to easily move subterms inside a product
Linear algebra
- sups: finite suprema/infima (a la bigop from ssreflect)
- 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)
Automata
- 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 partial derivatives
Completeness
- 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
Applications to program verification
- 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

Modules dependencies

Notes

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.

Authors

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-)

Acknowledgements

I am grateful to Thomas Braibant, with whom we developed the ancestor of this library, clearing the ground for this subsequent work.