regexp.abstract.automata.oneOrMore
Section Cxt.
Context {B St : finType}.
Context (mac : NFA B St).
Definition tr := trans mac.
Definition initial := start mac.
Definition terminal := final mac.
Definition startBack U := U :|: if inhabited (U :&: terminal) then initial else set0.
Definition mkTrans := [ffun b ⇒ [ffun st ⇒ startBack (tr b st)]].
Definition build : NFA B St :=
{|
trans := mkTrans;
start := initial;
final := terminal
|}.
Lemma liftStep {u v b} : step tr u v b → step mkTrans u v b.
rewrite /step /mkTrans /startBack ?ffunE; case (inhabited _) ⇒ h.
+ by apply /setUP; left.
+ by rewrite setU0.
Qed.
Lemma liftPath {xs} : ∀ u v, path.t tr u v xs → path.t mkTrans u v xs.
elim : xs ⇒ [|y ys IH]; move ⇒ u v.
- move /path.nilP ⇒ hu; by rewrite hu //=.
- case /path.consP ⇒ mid [hstep hpath].
set fstep := liftStep hstep.
apply /path.consP; ∃ mid; intuition.
Qed.
Lemma accept_one {xs} : accept mac xs → accept build xs.
case ⇒ u [hu [v [hv]]].
by move/liftPath ⇒ hpath; ∃ u; intuition; ∃ v; intuition.
Qed.
Lemma stepFinal {u v x} : step tr u v x → v \in terminal → ∀ w, w \in initial → step mkTrans u w x.
rewrite /step.
move ⇒ hstep hv w hw.
rewrite /step /mkTrans ?ffunE /startBack.
have hyp : inhabited (tr x u :&: terminal) by apply /existsP; ∃ v; apply/setIP.
by rewrite hyp; apply/setUP; right.
Qed.
Lemma reachable_cover {xs x} U : path.reachable tr U terminal (xs ++ [::x]) → path.cover mkTrans U initial (xs ++ [::x]).
case ⇒ u [hu]; case ⇒ w [hw] /path.snocP [mid [hpath hstep]].
move ⇒ v hv.
have hliftpath : path.t mkTrans u mid xs by apply liftPath.
∃ u; intuition.
suffices hstepv : step mkTrans mid v x by apply /path.snocP; ∃ mid.
by apply (stepFinal hstep).
Qed.
Lemma accept_cover {xs} : accept mac xs → path.cover mkTrans initial initial xs.
case (utils.snocE xs) ⇒ h.
- by rewrite h; move ⇒ _; apply (path.cover_nil initial).
- case: h ⇒ ys [y hxs].
rewrite hxs /accept -/initial -/terminal. apply /reachable_cover.
Qed.
Lemma accept_app {xs ys} : accept mac xs → accept build ys → accept build (xs ++ ys).
move ⇒ haccept.
set hcov := accept_cover haccept.
rewrite /accept -?/initial -?/terminal //= ⇒ hbuild.
by apply/(path.reachable_concat hcov).
Qed.
Lemma backward n : ∀ xs, (accept mac ^ (n.+1))%lan xs → accept build xs.
elim: n ⇒ [|n IH].
- by move ⇒ xs; rewrite (pow1 _ xs); apply accept_one.
- move: IH.
set m :=n.+1.
move ⇒ IH xs.
rewrite /pow -/pow.
case ⇒ ys [zs [hxs [hys hzs]]]; rewrite hxs.
set hacc := IH zs hzs.
by apply accept_app.
Qed.
Proof in forward direction
Fixpoint reach n U V xs :=
if n is m.+1 then ∃ ys zs, xs = ys ++ zs
∧ path.reachable tr U terminal ys
∧ reach m initial V zs
else path.reachable tr U V xs.
Lemma reach_accept : ∀ n xs, reach n initial terminal xs → (accept mac ^ (n.+1))%lan xs.
elim ⇒ [|n IHn]; move ⇒ xs.
- rewrite /reach ⇒ h.
by apply pow1; rewrite /accept.
- rewrite /reach -/reach ⇒ h.
case: h ⇒ ys [zs [hxs [hys hzs]]].
set haccept_ys : accept mac ys := hys.
set hind := IHn zs hzs.
move: hind; set m := n.+1.
move ⇒ hind; ∃ ys; intuition; ∃ zs; intuition.
Qed.
Lemma reach_cons {U V : {set St}} {x xs n} : reach n (neighbours tr U x) V xs → reach n U V (x :: xs).
elim: n ⇒ [|n IH].
- by apply path.neighbourhood_reachable.
- rewrite //=; case ⇒ ys [zs [hxs [hterm hreach]]].
∃ (x :: ys); ∃ zs; rewrite hxs; intuition.
by apply path.neighbourhood_reachable.
Qed.
Lemma bigStartBackU {rT : finType}{A : {set rT}} (F : rT → {set St}) :
startBack (\bigcup_(i in A) F i) = \bigcup_(i in A) startBack (F i).
rewrite /startBack -setP ⇒ u; apply/setUP/bigcupP.
- case ⇒ [/bigcupP h |].
+ by case: h ⇒ i hi hu; ∃ i; intuition; apply /setUP; left.
+ set hinhabited := inhabited _.
case (utils.lemb hinhabited ) ⇒ h; rewrite h ?in_set0.
× move: h; case /inhabitedIP ⇒ z [/bigcupP [i hi] hz hzt] hu.
suffices hyp : inhabited (F i :&: terminal) by [∃ i; intuition; rewrite hyp; apply /setUP; right].
by apply /inhabitedP; ∃ z; apply /setIP.
× done.
- case ⇒ i hi; case /setUP.
+ by left; apply /bigcupP; ∃ i.
+ set hinhabited := inhabited _.
case (utils.lemb hinhabited ) ⇒ h; rewrite h ?in_set0.
× move: h; case /inhabitedIP ⇒ z [hz hzt] hu.
suffices hyp : inhabited ( \bigcup_(i0 in A) F i0 :&: terminal) by rewrite hyp; right.
apply /inhabitedIP; ∃ z; split.
** by apply /bigcupP; ∃ i.
** done.
× done.
Qed.
Lemma neighbourhood (U : {set St}) x : neighbours mkTrans U x = startBack (neighbours tr U x).
rewrite bigStartBackU -setP ⇒ z.
apply /bigcupP /bigcupP;case ⇒ i hi; rewrite ?ffunE; ∃ i; rewrite ?ffunE; intuition.
Qed.
Lemma graded_reachability V xs : ∀ U, path.reachable mkTrans U V xs → ∃ n, reach n U V xs.
elim: xs ⇒ [|x xs IH].
- by move ⇒ U; ∃ 0.
- move ⇒ U; rewrite -path.neighbourhood_reachable.
rewrite neighbourhood /startBack.
set hin := inhabited _.
case (lemb hin) ⇒ h; rewrite h ?setU0 ?path.reachableULE.
+ case ⇒ /IH [n].
× by [∃ n; apply reach_cons].
× suffices hr : path.reachable tr U terminal [::x] by [∃ n.+1; ∃ [:: x]; ∃ xs; intuition].
by apply path.reachable1.
+ case /IH ⇒ [n]; by [∃ n; apply reach_cons].
Qed.
Lemma forward xs : accept build xs → ∃ n, (accept mac ^ (n.+1))%lan xs.
move/graded_reachability; rewrite -/initial -/terminal; case ⇒ [n]; by ∃ n; apply/reach_accept.
Qed.
Theorem correctness : accept build ≡ many1 (accept mac).
split.
- by apply/forward.
- by case ⇒ [n]; apply /backward.
Qed.
End Cxt.
if n is m.+1 then ∃ ys zs, xs = ys ++ zs
∧ path.reachable tr U terminal ys
∧ reach m initial V zs
else path.reachable tr U V xs.
Lemma reach_accept : ∀ n xs, reach n initial terminal xs → (accept mac ^ (n.+1))%lan xs.
elim ⇒ [|n IHn]; move ⇒ xs.
- rewrite /reach ⇒ h.
by apply pow1; rewrite /accept.
- rewrite /reach -/reach ⇒ h.
case: h ⇒ ys [zs [hxs [hys hzs]]].
set haccept_ys : accept mac ys := hys.
set hind := IHn zs hzs.
move: hind; set m := n.+1.
move ⇒ hind; ∃ ys; intuition; ∃ zs; intuition.
Qed.
Lemma reach_cons {U V : {set St}} {x xs n} : reach n (neighbours tr U x) V xs → reach n U V (x :: xs).
elim: n ⇒ [|n IH].
- by apply path.neighbourhood_reachable.
- rewrite //=; case ⇒ ys [zs [hxs [hterm hreach]]].
∃ (x :: ys); ∃ zs; rewrite hxs; intuition.
by apply path.neighbourhood_reachable.
Qed.
Lemma bigStartBackU {rT : finType}{A : {set rT}} (F : rT → {set St}) :
startBack (\bigcup_(i in A) F i) = \bigcup_(i in A) startBack (F i).
rewrite /startBack -setP ⇒ u; apply/setUP/bigcupP.
- case ⇒ [/bigcupP h |].
+ by case: h ⇒ i hi hu; ∃ i; intuition; apply /setUP; left.
+ set hinhabited := inhabited _.
case (utils.lemb hinhabited ) ⇒ h; rewrite h ?in_set0.
× move: h; case /inhabitedIP ⇒ z [/bigcupP [i hi] hz hzt] hu.
suffices hyp : inhabited (F i :&: terminal) by [∃ i; intuition; rewrite hyp; apply /setUP; right].
by apply /inhabitedP; ∃ z; apply /setIP.
× done.
- case ⇒ i hi; case /setUP.
+ by left; apply /bigcupP; ∃ i.
+ set hinhabited := inhabited _.
case (utils.lemb hinhabited ) ⇒ h; rewrite h ?in_set0.
× move: h; case /inhabitedIP ⇒ z [hz hzt] hu.
suffices hyp : inhabited ( \bigcup_(i0 in A) F i0 :&: terminal) by rewrite hyp; right.
apply /inhabitedIP; ∃ z; split.
** by apply /bigcupP; ∃ i.
** done.
× done.
Qed.
Lemma neighbourhood (U : {set St}) x : neighbours mkTrans U x = startBack (neighbours tr U x).
rewrite bigStartBackU -setP ⇒ z.
apply /bigcupP /bigcupP;case ⇒ i hi; rewrite ?ffunE; ∃ i; rewrite ?ffunE; intuition.
Qed.
Lemma graded_reachability V xs : ∀ U, path.reachable mkTrans U V xs → ∃ n, reach n U V xs.
elim: xs ⇒ [|x xs IH].
- by move ⇒ U; ∃ 0.
- move ⇒ U; rewrite -path.neighbourhood_reachable.
rewrite neighbourhood /startBack.
set hin := inhabited _.
case (lemb hin) ⇒ h; rewrite h ?setU0 ?path.reachableULE.
+ case ⇒ /IH [n].
× by [∃ n; apply reach_cons].
× suffices hr : path.reachable tr U terminal [::x] by [∃ n.+1; ∃ [:: x]; ∃ xs; intuition].
by apply path.reachable1.
+ case /IH ⇒ [n]; by [∃ n; apply reach_cons].
Qed.
Lemma forward xs : accept build xs → ∃ n, (accept mac ^ (n.+1))%lan xs.
move/graded_reachability; rewrite -/initial -/terminal; case ⇒ [n]; by ∃ n; apply/reach_accept.
Qed.
Theorem correctness : accept build ≡ many1 (accept mac).
split.
- by apply/forward.
- by case ⇒ [n]; apply /backward.
Qed.
End Cxt.