regexp.concrete.automata.build: Regexp to NFA - concrete layer

Overview

The building of automata in the concrete layer mimics the corresponding construction in the abstract layer.

re2nfa: Regular expression to NFA conversion.
correctness:Proof of correctness of re2nfa.

The re2nfa builds the automata recursively with one recursive step for each constructor. The proof is carried out by induction on the structure of the regular expression with one inductive step for each constructor.

The recursive steps themselves are nontrivial and hence we have packaged them in a module of their own (one for each constructor of the regular expression).

Require regexp.concrete.automata.alt.
Require regexp.concrete.automata.epsilon.
Require regexp.concrete.automata.concat.
Require regexp.concrete.automata.oneOrMore.
Require regexp.concrete.automata.singleton.

Just like the case of the abstract layer. Each of the above modules expose two functions

build: Which gives the appropriate construction
correctness: The correctness of the above construction.

Section Cxt.
  Context {B : sort}.
  Fixpoint State (re : expr.t B) : sort :=
    match re with
    | expr.eps ⇒ epsilon.State
    | expr.single _ ⇒ singleton.State
    | expr.alt re1 re2 ⇒ @alt.State (State re1) (State re2)
    | expr.concat re1 re2 ⇒ @concat.State (State re1) (State re2)
    | expr.many1 rep ⇒ State rep
    end.

  Lemma stateE (re : expr.t B) : universe.denote (State re) = abstract.automata.build.State re.
    elim: re ⇒ [|b|re1 IH1 re2 IH2| re1 IH1 re2 IH2| re IH]; by rewrite /universe.denote -/universe.denote //= ?IH1 ?IH2 ?IH.
  Qed.

  Fixpoint re2nfa (re : expr.t B) : NFA B (State re) :=
    match re with
    | expr.eps ⇒ epsilon.build
    | expr.single x ⇒ singleton.build x
    | expr.alt re1 re2 ⇒ alt.build (re2nfa re1) (re2nfa re2)
    | expr.concat re1 re2 ⇒ concat.build (re2nfa re1) (re2nfa re2)
    | expr.many1 rep ⇒ oneOrMore.build (re2nfa rep)
    end.

  Theorem correctness (re : expr.t B) : (accept (re2nfa re) ≡ expr.language re)%lan.
  Proof using Type.
    elim: re ⇒ [|b|re1 IH1 re2 IH2| re1 IH1 re2 IH2| re IH]; rewrite /expr.language -/expr.language.     - by rewrite epsilon.correctness.
    - by rewrite singleton.correctness.
    - by rewrite alt.correctness IH1 IH2.
    - by rewrite concat.correctness IH1 IH2.
    - by rewrite oneOrMore.correctness IH.
  Qed.

End Cxt.