regexp.abstract.automata.path

regexp.abstract.automata.path : Computational paths of an NFA

Paths in a transition system.

For a string xs : seq B, a computational path of the transition system labeled by letters of xs (in that order). An element γ : path xs u v should be seen as firing the transitions in the sequence xs and taking the machine (nondeterministically) from the state u to the state v.

One could define the path relation either as an inductive type. However, in this particular case, since all the types involved, i.e. the state space and the transition letter B are finite, we have defined path as a computable relation and hence is a bool instead of a Prop in the spirit of mathcomp style definitions. We proved the following views to get natural intutionistic content out of the path relation.

singleP Single step to path of single step.
nilP Empty paths and equality of endpoints.
consP Spliting the path into a step and the rest of the path
snocP Similar to consP but from the reverse side.

Section Path.
  Context {B St : finType}{tr : transition.t B St}.

  Fixpoint t (u v : St)(xs : seq B) : bool :=
    match xs with
    | [::] ⇒ u == v
    | y :: ys ⇒ [∃ mid, transition.step tr u mid y && t mid v ys]
    end.

A single step to path

  Lemma singleP (u v : St) b : reflect (step tr u v b) (t u v [:: b]).
    apply/(iffP existsP).
    - case ⇒ x /andP [hstep] /eqP heq; by rewrite -heq.
    - move ⇒ hstep; by ∃ v; apply/andP.
  Qed.

  Lemma consP {u v : St} {x xs} : reflect (∃ mid : St , step tr u mid x ∧ t mid v xs) (t u v (x :: xs)).
    rewrite //=; apply /(iffP existsP).
    - by case ⇒ z /andP h; ∃ z.
    - case ⇒ z [h1 h2]; ∃ z; by apply/andP.
  Qed.

  Lemma snocP {xs x} : ∀ u v, reflect (∃ mid : St , t u mid xs ∧ step tr mid v x) (t u v (xs ++ [:: x])).
  Proof using Type.
    elim: xs ⇒ [|z zs IH].
    - move ⇒ u v; rewrite //=; apply/(iffP existsP).
      + case ⇒ mid /andP [hstep /eqP hmidv]; ∃ u; by rewrite -hmidv.
      + case ⇒ mid [/eqP humid]; rewrite humid ⇒ hstep; ∃ v; apply/andP; split.
         × done.
         × by apply /eqP.
    - move ⇒ u v; rewrite //=; apply (iffP existsP).
      + case ⇒ mid0 /andP [hstepu] /(IH mid0 v) [mid1 [hmidpath hstep]].
        ∃ mid1; split.
        × by apply/existsP; ∃ mid0; apply /andP.
        × done.
      + case ⇒ mid1 [hyp] hstep1. case /existsP : hyp ⇒ mid0 /andP [hstep2 hpath];
                                        ∃ mid0; apply /andP; split.
        × done.
        × apply /IH; ∃ mid1; split; done.
  Qed.

  Definition nilP {u v : St} : reflect (u = v) (t u v [::]) := eqP.
  Check nilP.

  Lemma concat {xs} : ∀ {u v}, t u v xs → ∀ {w ys}, t v w ys → t u w (xs ++ ys).
    elim xs ⇒ [|z zs IH].
    - move ⇒ u v; move/nilP ⇒ h; by rewrite h.
    - move ⇒ u v. case/consP ⇒ mid [hstep p1].
      move ⇒ w ys p2. apply/consP; ∃ mid; split.
      + done.
      + by apply/(IH mid v).
  Qed.

End Path.
Arguments t {B St} tr.

Accessability relation

Module access.

  Section Cxt.
    Context {B St : finType}{tr : transition.t B St}.
    Definition to (u : St)(V : {set St})(xs : seq B) := ∃ v , v \in V ∧ path.t tr u v xs.
    Definition from (U : {set St}) v xs := ∃ u , u \in U ∧ path.t tr u v xs.

    Definition single_to {u v : St}(xs : seq B) : path.t tr u v xs → to u [set v] xs.
      move ⇒ hpath; by ∃ v; rewrite in_set1 eqxx; intuition.
    Qed.

    Definition single_from {u v : St}(xs : seq B) : path.t tr u v xs → from [set u] v xs.
      move ⇒ hpath; by ∃ u; rewrite in_set1 eqxx; intuition.
    Qed.

    Definition cons {u mid : St}{V}{x : B}{xs : seq B}
      : transition.step tr u mid x → to mid V xs → to u V (x :: xs).
      move ⇒ hstep; case ⇒ v [hv hpath]; ∃ v; intuition. apply /consP; ∃ mid; intuition.
    Qed.

    Lemma toU {u : St}{V1 V2 : {set St}} : ∀ xs, to u (V1 :|: V2) xs ↔ to u V1 xs ∨ to u V2 xs.
      move ⇒ xs; split; rewrite /to ⇒ h.
      - case: h ⇒ v; rewrite in_setU -(rwP orP);
                  case ⇒ [[hv1|hv2] hpath]; [left|right]; ∃ v; intuition.
      - case: h ⇒ h; case: h ⇒ v [hv hpath]; ∃ v; rewrite in_set -(rwP orP); intuition.
    Qed.

    Lemma fromU {U1 U2 : {set St}}{v} : ∀ xs, from (U1 :|: U2) v xs ↔ from U1 v xs ∨ from U2 v xs.
      move ⇒ xs; split; rewrite /from ⇒ h.
      - case: h ⇒ u; rewrite in_setU -(rwP orP);
                  case ⇒ [[hu1|hu2] hpath]; [left|right]; ∃ u; intuition.
       case: h ⇒ h; case: h ⇒ u [hu hpath]; ∃ u; rewrite in_set -(rwP orP); intuition.
    Qed.

    Lemma tosub {u : St}{V1 V2 : {set St}} : {subset V1 ≤ V2 } → ∀ xs, to u V1 xs → to u V2 xs.
    Proof using Type.
      move ⇒ hsub xs hex.
      case: hex ⇒ v [hv hpath]; ∃ v; split.
      - by apply/hsub.
      - done.
    Qed.

    Lemma fromsub {U1 U2 : {set St}}{v} : {subset U1 ≤ U2 } → ∀ xs, from U1 v xs → from U2 v xs.
    Proof using Type.
      move ⇒ hsub xs hex.
      case: hex ⇒ u [hu hpath]; ∃ u; split.
      - by apply/hsub.
      - done.
    Qed.

  End Cxt.

  Arguments to {B St} tr.
  Arguments from {B St} tr.
End access.

Reachability and cover.

Two important relation between two subset of states is reachability and cover defined thus. By reachable we mean there is an access to a vertex in V from U. By cover we mean the vertices of V are path covered by the bunch of paths originating in U.

Section Cxt.

  Context {B St : finType}{tr : transition.t B St}.

  Definition reachable (U V : {set St}) (xs : seq B) := ∃ u , u \in U ∧ access.to tr u V xs.
  Definition cover (U V : {set St})(xs : seq B) := ∀ v, v \in V → access.from tr U v xs.

  Lemma reachable1 {U V x} : inhabited (neighbours tr U x :&: V) → reachable U V [::x].
    case /inhabitedIP ⇒ z [/bigcupP hneigh] hV.
    by case: hneigh ⇒ u hu hstep; ∃ u; intuition; ∃ z; intuition; apply/singleP.
  Qed.

  Lemma reachableULE (U1 U2 V: {set St})(xs : seq B) : reachable (U1 :|: U2) V xs ↔ reachable U1 V xs ∨ reachable U2 V xs.
    rewrite /reachable; split.
    - case ⇒ u; rewrite in_setU -(rwP orP).
      by case ⇒ [[hu1|hu2] haccess]; [left|right]; ∃ u; intuition.
    - by case ⇒ hyp; case: hyp ⇒ u haccess; ∃ u; rewrite in_setU -(rwP orP); intuition.
  Qed.

  Lemma reachableURE (U V1 V2: {set St})(xs : seq B) : reachable U (V1 :|: V2) xs ↔ reachable U V1 xs ∨ reachable U V2 xs.
    rewrite /reachable; split.
    - case ⇒ u [hu haccess].
      suffices hyp : access.to tr u V1 xs ∨ access.to tr u V2 xs by case hyp; [left| right]; ∃ u.
      by rewrite -access.toU.
    - by case ⇒ hyp; case: hyp ⇒ u [hu haccess]; ∃ u; rewrite access.toU; intuition.
  Qed.

  Lemma cover_nil (U : {set St}) : cover U U [::].
  Proof using Type.
    rewrite /cover ⇒ v hv.
    ∃ v; by rewrite /t eqxx.
  Qed.

  Lemma neighbourhood_cover (U : {set St}) b : cover U (transition.neighbours tr U b) [::b].
    rewrite /neighbours /cover.
    move ⇒ v; case/bigcupP ⇒ u hu hv; ∃ u; intuition; by apply /singleP.
  Qed.

  Lemma cover_concat {U V W : {set St}} xs ys : cover U V xs → cover V W ys → cover U W (xs ++ ys).
    move ⇒ hUV hVW w hw.
    set hmidw := hVW w hw.
    case: hmidw ⇒ mid [hmid pmidw].
    set humid := hUV mid hmid.
    case: humid ⇒ u [hu pumid].
    ∃ u; split.
    - done.
    - exact: (path.concat pumid pmidw).
  Qed.

  Lemma cover_supL {U V1 V2 : {set St}} : {subset V1 ≤ V2 } → ∀ xs, cover U V2 xs → cover U V1 xs.
    move ⇒ hsup xs; rewrite /cover ⇒ hV2.
    move ⇒ v hv.
    suffices h : v \in V2 by apply (hV2 v).
    by apply hsup.
  Qed.

  Lemma cover_subR {U1 U2 V : {set St}} : {subset U1 ≤ U2 } → ∀ xs, cover U1 V xs → cover U2 V xs.
    move ⇒ hsub xs. rewrite /cover ⇒ hU1.
    by move ⇒ v hv; apply/(access.fromsub hsub); exact: hU1 v hv.
  Qed.

  Lemma reachable_concat {U V W : {set St}}{xs ys : seq B} : cover U V xs → reachable V W ys → reachable U W (xs ++ ys).
    rewrite /cover /reachable ⇒ hcov hreach.
    case: hreach ⇒ mid [hmid [v [hv Pmidv]]].
    set hu := hcov mid hmid.
    case: hu ⇒ u [hu Pumid].
    ∃ u; intuition; ∃ v; intuition; by apply (concat (v:=mid)).
  Qed.

  Lemma neighbourhood_reachable {U V : {set St}} {x xs} : reachable (neighbours tr U x) V xs ↔ reachable U V (x :: xs).
    split ⇒ h.
    - by rewrite -/(app [::x] xs); apply (reachable_concat (neighbourhood_cover U x)).
    - case: h ⇒ u [hu hacc].
      case: hacc ⇒ v [hv].
      case /consP ⇒ mid [hstep hpath].
      ∃ mid; rewrite /neighbours; split.
      + by apply /bigcupP; ∃ u.
      + by ∃ v.
  Qed.

  Definition deadEnd u := ∀ st b, transition.step tr u st b = false.

  Definition nopathP {u} : deadEnd u → ∀ x xs st, reflect (path.t tr u st (x :: xs)) false.
    move ⇒ hdead x xs st; apply/ReflectF; apply/negP.
    apply/consP; case ⇒ mid; rewrite hdead; by case ⇒ h1.
  Qed.

  Lemma trivialpathP {u st} : deadEnd u → ∀ xs, reflect (xs = [::] ∧ st = u) (path.t tr u st xs).
    move ⇒ hdead; case ⇒ [|z zs].
    - apply/(iffP nilP); by intuition.
    - apply/(iffP idP).
      × case/existsP ⇒ x; by rewrite hdead //=.
      × by case ⇒ h; inversion h.
  Qed.

End Cxt.

Arguments reachable {B St} tr.
Arguments cover {B St} tr.
Arguments deadEnd {B St} tr.

Automata on direct sum of states

The automata construction for the r1 | r2 (choice operation) as well as r1 . r2 (concatenation) makes use of the direct sum of the state spaces. Here are a few lemma that refactors various reachability lemma that is common for these two cases.

Section Matrix.
  Context {B St0 St1 : finType}.

  Context {tr0 : transition.t B St0}
    {r01 : {ffun B → relation.t St0 St1}}
    {tr1 : transition.t B St1}.

  Lemma noPathLRE {xs} : ∀ {u v}, path.t (transition.diagonal tr0 tr1) (inl u) (inr v) xs = false.
  Proof using Type.
    elim: xs ⇒ [|y ys IH].
    - move ⇒ u v.
      apply/path.nilP ⇒ h; inversion h.
    - move ⇒ u v.
      apply /path.consP.
        case ⇒ mid; case: mid ⇒ st; rewrite ?IH ?noStepLRE; by case.
  Qed.

  Lemma unReachableLR (U : {set St0})(V : {set St1})
    : ∀ xs, ¬ path.reachable (transition.diagonal tr0 tr1) (inl @: U) (inr @: V) xs.
    move ⇒ xs; rewrite /path.reachable.
    case ⇒ u; case: u ⇒ u; case ⇒ hu [v];
                                  case: v ⇒ v; move: hu;
                                                    rewrite ?imset_inr_inl ?imset_inl_inr ?noPathLRE; by move ⇒ hu [hv].
  Qed.

  Definition tr := utmatrix tr0 r01 tr1.
  Lemma noPathRLE {xs} : ∀ {u v}, path.t tr (inr u) (inl v) xs = false.
  Proof using Type.
    elim: xs ⇒ [|y ys IH].
    - move ⇒ u v; apply/path.nilP ⇒ h; inversion h.
    - move ⇒ u v.
      apply /path.consP;
        case ⇒ mid; case: mid ⇒ st; rewrite ?IH ?noStepRLE; by case.
  Qed.

  Lemma pathLP {xs} : ∀ u v, reflect (path.t tr0 u v xs) (path.t tr (inl u) (inl v) xs).
  Proof using Type.
    elim xs ⇒ [|y ys IH].
    - move ⇒ u v; rewrite /path.t /eq_op //= -/eq_op.
      by exact idP.
    - move ⇒ u v; apply/(iffP path.consP).
      + case ⇒ mid; case: mid ⇒ mid.
        × rewrite -(rwP (stepLP u mid)) -(rwP (IH mid v)); intuition; apply /existsP; ∃ mid; by apply /andP.
        × rewrite noPathRLE; by intuition.
      + case/path.consP ⇒ mid; case ⇒ hstep hpath; ∃ (inl mid); split.
        × by apply /stepLP.
        × by apply /IH.
  Qed.

  Lemma pathRP {xs} : ∀ u v, reflect (path.t tr1 u v xs) (path.t tr (inr u) (inr v) xs).
  Proof using Type.
    elim xs ⇒ [|y ys IH].
    - move ⇒ u v; rewrite /path.t /eq_op //= -/eq_op; by exact idP.
    - move ⇒ u v; apply/(iffP path.consP).
      + case ⇒ mid; case: mid ⇒ mid.
        × rewrite noStepRLE; by intuition.
        × rewrite -(rwP (stepRP u mid)) -(rwP (IH mid v)); intuition; apply /existsP; ∃ mid; by apply /andP.
      + case/path.consP ⇒ mid; case ⇒ hstep hpath; ∃ (inr mid); split.
        × by apply /stepRP.
        × by apply /IH.
  Qed.

  Lemma reachableLL (U V : {set St0}) : ∀ xs, path.reachable tr0 U V xs ↔ path.reachable tr (inl @: U) (inl @: V) xs.
    move ⇒ xs; rewrite /path.reachable; split.
    - case ⇒ u [hu [v [hv]]]. move/pathLP ⇒ hpath; ∃ (inl u); rewrite imset_inl; intuition; ∃ (inl v); rewrite imset_inl; intuition.
    - case ⇒ u; case: u ⇒ u; rewrite ?imset_inl ?imset_inr_inl.
      + case ⇒ hu hto; case: hto ⇒ v; case: v ⇒ v; rewrite ?imset_inl ?imset_inr_inl.
        × case ⇒ hv; move/pathLP ⇒ hpath; ∃ u; intuition; ∃ v; intuition.
        × intuition.
      + intuition.
  Qed.

  Lemma reachableRR (U V : {set St1}) : ∀ xs, path.reachable tr1 U V xs ↔ path.reachable tr (inr @: U) (inr @: V) xs.
  Proof using Type.
    move ⇒ xs; rewrite /path.reachable; split.
    - case ⇒ u [hu [v [hv]]]; move/pathRP ⇒ hpath; ∃ (inr u); rewrite imset_inr; intuition; ∃ (inr v); rewrite imset_inr; intuition.
    - case ⇒ u; case: u ⇒ u; rewrite ?imset_inr ?imset_inl_inr.
      + intuition.
      + case ⇒ hu hto; case: hto ⇒ v; case: v ⇒ v; rewrite ?imset_inr ?imset_inl_inr.
        × intuition.
        × case ⇒ hv; move/pathRP ⇒ hpath; ∃ u; intuition; ∃ v; intuition.
  Qed.

  Lemma unReachableRL (U : {set St1})(V : {set St0}) : ∀ xs, ¬ path.reachable tr (inr @: U) (inl @: V) xs.
  Proof using Type.
    move ⇒ xs; rewrite /path.reachable.
    case ⇒ u; case: u ⇒ u; case ⇒ hu [v]; case: v ⇒ v; move: hu;
                           rewrite ?imset_inr_inl ?imset_inl_inr ?noPathRLE; by move ⇒ hu [hv].
  Qed.

End Matrix.