Deciding Kleene Algebras in Coq

TL;DR

This paper introduces a Coq tactic that efficiently decides equations in Kleene algebras using automata algorithms, formal correctness proofs, and algebraic reasoning, enabling scalable and reliable verification.

Contribution

The paper presents a formally verified, scalable decision procedure for Kleene algebra equations implemented as a Coq tactic, leveraging automata algorithms and algebraic formalization.

Findings

The tactic solves equations instantaneously for casual cases.

It scales effectively to larger algebraic expressions.

Correctness is formally proven using Kozen's initiality theorem.

Abstract

We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The decision procedure is proved correct and complete: correctness is established w.r.t. any model by formalising Kozen's initiality theorem; a counter-example is returned when the given equation does not hold. The correctness proof is challenging: it involves both a precise analysis of the underlying automata algorithms and a lot of algebraic reasoning. In particular, we have to formalise the theory of matrices over a Kleene algebra. We build on the recent addition of firstorder typeclasses in Coq in order to work efficiently with the involved algebraic structures.