Nominal Kleene Algebra

Coq proof

Coq files and Documentation

This proof is decomposed in a number of modules, dealing with different aspects.

  • tools

    (link)This module contains simple notations, definitions, tactics and lemmas, mostly independant of the rest of the developpement.
  • atoms

    (link)Here we simply define atoms, and permutations of atoms.
  • atoms_ops

    (link)This library defines a number of operations on lists of atoms.
  • equiv_lst

    (link)Defines an equivalence relation on lists of atoms.
  • letter

    (link)Introduces letters.
  • expr

    (link)The type of expressions is defined, together with some elementary functions such as size, equality...
  • predicates

    (link)We define in this library some predicates over expressions, such as typing, freshness...
  • morphisms

    (link)The important functions manipulating expressions can be found here.
  • proofs

    (link)In this library the generic proof system is defined, as well as the various axiom bundles.
  • rm0

    (link)The technical proofs dealing with bridges between positive and non-positive theories.
  • removetype

    (link)The technical proofs dealing with bridges between typed and untyped theories.
  • perm

    (link)The technical proofs dealing with bridges between theories with our without explicit permutations.
  • theories

    (link)Definition of the different theories, and stability results about them.
  • sg_to_mlt

    (link)The technical proofs dealing with bridges from atomic to literate theories.
  • order

    (link)Definitions of the preorder relations on theories, and proofs of the ordering of our theories.
  • restr_atoms,normalise

    (link1, link2) The other files are still in a preliminary state.