regexp.concrete.automata.oneOrMore

Section Cxt.

  Context {B St : sort}.
  Context (mac : NFA B St).
  Definition tr := trans mac.
  Definition initial := start mac.
  Definition terminal := final mac.

  Definition startBack U := (if inhabited (U ∩ terminal) then union U initial else U)%con.

  Lemma startBack_denote U : subset.denote (startBack U) = oneOrMore.startBack (automata.denote mac) (subset.denote U).
    rewrite /startBack /oneOrMore.startBack subset.inhabited_spec subset.intersection_spec /terminal //=.
    case (utils.inhabited _); by rewrite ?subset.union_spec ?setU0.
  Qed.

  Definition mkTrans := map (map startBack) tr.

  Definition build : NFA B St :=
    {|
      trans := mkTrans;
      start := initial;
      final := terminal
    |}.

  Lemma equality : automata.denote build = (abstract.automata.oneOrMore.build (automata.denote mac)).
  Proof using Type.
    apply abstract.automata.eq_equiv.
    rewrite /automata.equiv //=; intuition; apply /eqP.
    rewrite /mkTrans /oneOrMore.mkTrans -?ffunP ⇒ x.
    rewrite function.denoteE ?function.to_map ?ffunE -?ffunP ⇒ y.
    by do 2 rewrite ?function.denoteE ?ffunE ?function.to_map ?startBack_denote.
  Qed.

  Theorem correctness : (accept build ≡ many1 (accept mac))%lan.
  Proof using Type.
    by rewrite /accept equality abstract.automata.oneOrMore.correctness.
  Qed.

End Cxt.