regexp.abstract.automata.concat


Section Cxt.

Automata construction for concatenation

The construction is parametrised over the following

The alphabet set B.

The automata macL and macR with state spaces StL and StR

respectively

  Context {B : finType}.

  Context {St0 : finType}(mac0 : NFA B St0).
  Context {St1 : finType}(mac1 : NFA B St1).

  Definition State : finType := (St0 + St1)%type.

  Definition tr0 := trans mac0.
  Definition tr1 := trans mac1.

  Definition start0 := start mac0.
  Definition start1 := start mac1.

  Definition final0 := final mac0.
  Definition final1 := final mac1.

  Definition hasfinal0 U := inhabited (U :&: final0).
  Definition prefinal0 y st := hasfinal0 (trans mac0 y st).

  Definition rel01 : {ffun B → relation.t St0 St1} :=
    [ffun y ⇒ [ffun st ⇒ if prefinal0 y st then start1 else set0]].

  Definition mkTrans : transition.t B State := transition.utmatrix tr0 rel01 tr1.

The initial state is the starting state of
  Definition initial : {set State} := if hasfinal0 start0 then inl @: start0 :|: inr @: start1 else inl @: start0.
  Definition terminal : {set State} := inr @: final1.

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

  Lemma start0_subset_initial : {subset inl @: start0 ≤ initial}.
    apply /subsetP.
    rewrite /initial; case hasfinal0.
    - by apply subsetUl.
    - by apply subxx.
  Qed.

  Lemma in_initialL {u} : (inl u) \in initial → u \in start0.
    rewrite /initial; case hasfinal0.
    case /setUP; by rewrite ?imset_inl_inr ?imset_inl.
    by rewrite ?imset_inl.
  Qed.

  Lemma in_initialR {v} : inr v \in initial → accept mac0 [::] ∧ v \in start1.
    rewrite /initial ⇒ h.
    have hyp : hasfinal0 start0. move : h; case hasfinal0.
    - done.
    - by rewrite imset_inr_inl.
      split.
      + by move: hyp; case /existsP ⇒ u /setIP [hstart hfinal]; ∃ u; intuition; ∃ u; intuition; rewrite /path.t.
      + by move: h; rewrite hyp; case /setUP; by rewrite ?imset_inr_inl ?imset_inr.
  Qed.

Right to left paths

The transition function of the concatenation operation is very similar to that of choice. The additional transitions are only between the left and the right states. As a result we have the following properties.
1. Any path in the left automata can be lifted to a path in the concatenation automata pathLP.
2. Any path in the right automata can be lifted to a path in the concatenation automata pathRP.
3. There are no cross paths from the right states noPathRLE to the left states because there are no such transition nostepRLE.
4. The cross path between left and right states can be appropriately split.

 Lemma stepLRP {u v b} :
   reflect (v \in start1 ∧ ∃ mid, transition.step tr0 u mid b ∧ mid \in final0) (transition.step mkTrans (inl u) (inr v) b).
   apply/(iffP idP); rewrite /transition.step /mkTrans ?ffunE.
   - case /setUP.
     + by rewrite imset_inr_inl.
     + rewrite /prefinal0 /hasfinal0 /inhabited.
       set htest := [∃ z, z \in trans mac0 b u :&: final0].
       have hyp : htest ∨ htest = false by case htest; intuition.
       case: hyp ⇒ hcase.
       × rewrite imset_inr; rewrite hcase; split.
         ** done.
         ** have h1 : ∃ z, z \in tr0 b u :&: final0 by apply /existsP.
            by case: h1 ⇒ mid /setIP h2; ∃ mid.
       × by rewrite hcase imset0 in_set0.
   - case ⇒ hv hmid; apply/setUP; right.

     suffices hyp : prefinal0 b u by rewrite hyp imset_inr.

     case: hmid ⇒ mid hmid.
     rewrite /prefinal0 /hasfinal0; apply /existsP; ∃ mid.
     by apply/setIP.
 Qed.

  Lemma coverLRE xs x {U} : path.reachable tr0 U final0 (xs ++ [:: x]) →
                            path.cover mkTrans (inl @: U) (inr @: start1) (xs ++ [:: x]).
    case ⇒ u [hu] [v [hv]].
    case /path.snocP ⇒ mid [hpath hstep].
    have hyp : ∀ w, w \in start1 → transition.step mkTrans (inl mid) (inr w) x
          by move ⇒ w hstart; apply /stepLRP; intuition; ∃ v; intuition.

    case ⇒ w; rewrite ?imset_inl_inr ?imset_inr.
    - done.
    - move ⇒ hw; ∃ (inl u); intuition.
      + by rewrite imset_inl.
      + by apply /path.snocP; ∃ (inl mid); intuition; apply/path.pathLP.
  Qed.

  Lemma accept_nil : accept mac0 [::] → ∀ st, st \in start1 ↔ inr st \in initial.
  Proof.
    rewrite /accept /path.reachable.
    case ⇒ u [hu [v [hv /path.nilP huv]]]; move: hu hv; rewrite huv ⇒ h1 h2.
    have hyp : hasfinal0 start0 = true by rewrite /hasfinal0; apply/existsP; ∃ v; apply /setIP.
    have hinitial : initial = inl @: start0 :|: inr @: start1 by rewrite /initial hyp.
    constructor; rewrite hinitial.
    - by move ⇒ h; apply /setUP; right; rewrite imset_inr.
    - case /setUP; by rewrite ?imset_inr_inl ?imset_inr.
  Qed.

  Lemma cover_start1 {xs : seq B} : accept mac0 xs → path.cover mkTrans initial (inr @: start1) xs.
    case (snocE xs) ⇒ h.
    - rewrite h; move/accept_nil ⇒ hyp.
      suffices hsubset : {subset inr @: start1 ≤ initial} by apply (path.cover_supL hsubset); apply path.cover_nil.
      move ⇒ st; case: st ⇒ st; rewrite ?imset_inl_inr ?imset_inr.
      × done.
      × by apply hyp.
    - case: h ⇒ ys [y hxs]. rewrite hxs /accept ⇒ hreach.

      suffices hsubset : {subset inl @: start0 ≤ initial} by apply (path.cover_subR hsubset); apply coverLRE.
      apply start0_subset_initial.
  Qed.

  Lemma concat_accept : ∀ xs ys, accept mac0 xs ∧ accept mac1 ys → accept build (xs ++ ys).
  Proof using Type.
    move ⇒ xs ys [hxs hys].

    have haccess : path.cover mkTrans initial (inr @: start1) xs by apply/cover_start1.
    have hreach : path.reachable mkTrans (inr @: start1) terminal ys. rewrite /terminal -path.reachableRR; apply/hys.
    apply/(path.reachable_concat haccess hreach).
  Qed.

  Lemma pathLRE xs : ∀ {u v}, path.t mkTrans (inl u) (inr v) xs → ∃ ys zs, xs = ys ++ zs
                                                                            ∧ path.access.to tr0 u final0 ys
                                                                            ∧ path.access.from tr1 start1 v zs.
  Proof.
    elim: xs ⇒ [|x xs IH].
    - move ⇒ u v; move/path.nilP ⇒ h; inversion h.
    - move ⇒ u v.
      case /path.consP ⇒ mid; case: mid ⇒ mid [hstep hpath].
      + set hyp := IH _ _ hpath.
        case: hyp ⇒ ys [zs [hxs [hto hfrom]]]; ∃ (x :: ys); ∃ zs; intuition.
        × by rewrite hxs.
        × suffices hyp: step tr0 u mid x by apply /(path.access.cons hyp hto).
          by apply /transition.stepLP; exact: hstep.
      + move: hstep; case/stepLRP ⇒ hmidstart [fmid [hfstep hfmidfinal]].
         ∃ [:: x]; ∃ xs; intuition.
         × by [∃ fmid; intuition; apply /path.singleP].
         × by ∃ mid; intuition; apply/path.pathRP; exact: hpath.
  Qed.

  Lemma accept_concat : ∀ xs, accept build xs → ∃ ys zs, xs = ys ++ zs ∧ accept mac0 ys ∧ accept mac1 zs.
  Proof.
    move ⇒ xs; case ⇒ u; case: u ⇒ u; rewrite /build /start /terminal //=; case ⇒ hu haccess.
    - case: haccess ⇒ v; case: v ⇒ v; rewrite ?imset_inl_inr ?imset_inr.
      + by case.
      + case ⇒ hv hpath.
        set hyp := pathLRE xs hpath.
        case: hyp ⇒ ys [zs [hxs [ha1 ha2]]].
        set hustart0 := in_initialL hu; ∃ ys; ∃ zs; intuition.
        × by ∃ u.
        × by case ha2 ⇒ mid [hmid] hpath1; ∃ mid; intuition; ∃ v; intuition.
    - set hyp := in_initialR hu; case: hyp ⇒ hinit haccept.
      ∃ [::]; ∃ xs; intuition.
      rewrite /accept path.reachableRR.
      by ∃ (inr u); rewrite imset_inr; intuition; apply haccess.
  Qed.

  Theorem correctness : accept build ≡ (accept mac0 ++ accept mac1)%lan.
    split.
    - by apply accept_concat.
    - by case ⇒ ys [zs [hxs]]; rewrite hxs; apply concat_accept.
  Qed.

End Cxt.