Library fl.aut.re_fa

Require Import automata regexp misc.

Set Implicit Arguments.

Section RE_FA.
  Import Automata.

  Variable char: finType.
  Definition word:= word char.

  Fixpoint re_to_dfa (r: regular_expression char): dfa char :=
    match r with
    | Void ⇒ dfa_void char
    | Eps ⇒ dfa_eps char
    | Dot ⇒ dfa_dot char
    | Atom a ⇒ dfa_char char a
    | Star s ⇒ nfa_star (dfa_to_nfa (re_to_dfa s))
    | Plus s t ⇒ dfa_disj (re_to_dfa s) (re_to_dfa t)
    | And s t ⇒ dfa_conj (re_to_dfa s) (re_to_dfa t)
    | Conc s t ⇒ nfa_to_dfa (nfa_conc (dfa_to_nfa (re_to_dfa s)) (dfa_to_nfa (re_to_dfa t)))
    | Not s ⇒ dfa_compl (re_to_dfa s)
    end.

  Lemma re_to_dfa_correct r: dfa_lang (re_to_dfa r) =i r.
    (* Star *)

  Definition re_equiv r s := dfa_equiv (re_to_dfa r) (re_to_dfa s).

  Lemma re_equiv_correct r s: re_equiv r s ↔ r =i s.

End RE_FA.