LangAlg

A complete axiomatization of the algebra of languages over the signature of reversible Kleene lattices, proved in Coq.

What is this repository for?

This repository contains the full proof. The documentation is also available on my personal webapge, here.

How do I get set up?

This proof was developped using Coq version 8.8.1. To download the proof, simply run the command:

git clone git@github.com:monstrencage/LangAlg.git

We generated a Makefile automatically using the tool coq_makefile. The documentation for this tool can be found here. To generate the Makefile, run the command:

coq_makefile -f _CoqProject -o Makefile

Then the proof can be compiled and its documentation generated by calling:

make gallinahtml

For readability reasons, we heavily use utf-8 symbols.

This proof was developed using emacs with Proof General and company-coq.

Overview of the proof

• tools Toolbox of simple definitions, lemmas and tactics.

• language Basics of languages.

• prime_set Simple facts about sets obtained by duplication.

• klm Identity-free Kleene lattices

• one_free_expr Expressions without the constant 1

• lklc Definition and equational theory of reversible Kleene lattices.

• lklc_lang Language interpretation of expressions from lklc.

• lklc_reduction Important intermediary steps towards a reduction from lklc to one_free_expr.

• completeness We finally arrive to the main result of this development: the proof that our axiomatization is complete for the equational theory of languages.

• top Some facts about adding the constant top to the signature.