Position Automata

This directory is a small Coq project for modeling position automata (Glushkov automata) for regular expressions.

It is intended to live next to the Linden development and to reuse the same Coq/opam environment:

cd /home/linden
eval $(opam env)
dune build
cd position-automata
dune build

The project currently contains:

• Syntax.v: source regular expressions, positioned regular expressions, and the recursive labeling pass.
• Sets.v: lightweight finite-set operations over lists of positions.
• KleeneSemantics.v: Kleene-style language semantics for regexes together with the semantic-preservation theorem for the labeling pass.
• PositionAutomaton.v: nullable, first/last/follow positions, and the associated automaton, plus a standard marked-word acceptance predicate for the corresponding Glushkov position automaton.
• PositionCorrectness.v: foundational lemmas for the correctness proof, in particular that label generates a contiguous, duplicate-free sequence of positions.
• Equivalence.v: a fuel-bounded executable equivalence checker with a Coq soundness theorem for deterministic automata over a finite alphabet.
• Examples.v: tiny executable examples.
• LindenBridge.v: imports Linden/Warblre modules and is the intended place for translations to and from Linden's regex syntax.

The generated position-automata.opam file is produced from dune-project.

Current proof status:

• done: regex/Kleene semantics <-> marked semantics after labeling;
• done: a standard marked-word acceptance definition for the position automaton;
• done: uniqueness of positions generated by label;
• not yet done: the full Coq theorem that matches_marked is equivalent to accepts_marked, and therefore that regex semantics is equivalent to position-automaton acceptance.