package coq-atbr

This library provides algebraic tools for working with binary relations. The main tactic provided is a reflexive tactic for solving (in)equations in an arbitrary Kleene algebra. The decision procedure goes through standard finite automata constructions.

Note that the initial authors consider this library to be superseded by the Relation Algebra library, which is based on derivatives rather than automata: https://github.com/damien-pous/relation-algebra