Library fl.aut.transitive_closure
Require Import Recdef.
Require Import automata misc regexp re_standard re_fa.
Set Implicit Arguments.
Import Prenex Implicits.
Import Automata.
Lemma set1UrP (T: finType) (X: {set T}) x: reflect (x |: X = X) (x \in X).
Lemma plusP {char} r s (w: word char):
reflect (w \in r ∨ w \in s)
(w \in plus r s).
Lemma set_pick_size {F: finType} (X: {set F}) z: [pick z in X] = Some z → #|X :\ z| < #|X|.
Lemma setU1_predI {F: finType} (X: {set F}) z: (z \notin X) → (mem X) =1 predI (mem (z |: X)) (predC (pred1 z)).
Lemma all_predD {X} (q p: pred X) xs: all (predD q p) xs = all q xs && all (predC p) xs.
Section AllButLastDef.
Variable X: Type.
Variable p: pred X.
Fixpoint belast (xs: seq X) :=
match xs with
| [::] ⇒ [::]
| [::x] ⇒ [::]
| x::xs ⇒ x::(belast xs)
end.
Lemma belast_rcons (x: X) xs:
belast (rcons xs x) = xs.
Definition allbutlast xs := all p (belast xs).
End AllButLastDef.
Implicit Arguments allbutlast [X].
Section AllButLast.
Variable X: Type.
Variable p q: pred X.
(* p => q -> allbutlast p -> allbutlast q *)
Lemma allbutlast_impl xs:
subpred p q →
allbutlast p xs →
allbutlast q xs.
Lemma allbutlast_nil: allbutlast p [::] = true.
Lemma allbutlast_cons x xs: p x → allbutlast p xs → allbutlast p (x::xs).
(* if at least one element in xs is actually
applied to p we can extract that application. *)
Lemma allbutlast_cons' x y xs: allbutlast p (x::y::xs) → p x && allbutlast p (y::xs).
(* if p holds everywhere on xs, it also holds
for all but the last element *)
Lemma all_allbutlast xs: all p xs → allbutlast p xs.
(* we can either extract an application of p x or
x is the last element in x::xs (i.e. xs is empty). *)
Lemma allbutlast_cons'' x (xs: seq X): allbutlast p (x::xs) → (size xs == 0) || (p x && allbutlast p xs).
(* all .. + allbutlast .. -> allbutlast (.. + ..) *)
Lemma all_allbutlast_cat xs ys: all p xs → allbutlast p ys → allbutlast p (xs++ys).
Lemma allbutlast_cat xs ys: allbutlast p (xs++ys) → allbutlast p xs ∧ allbutlast p ys.
(* with p (last xs) we can extend allbutlast to all. *)
Lemma allbutlast_last x xs: allbutlast p xs → p (last x xs) → all p xs.
(* constant false can only hold for one element or fewer. *)
Lemma allbutlast_pred0 xs: p =1 pred0 → allbutlast p xs → size xs ≤ 1.
Lemma allbutlast_predI xs: allbutlast (predI p q) xs = allbutlast p xs && allbutlast q xs.
Lemma allbutlast_predD xs: allbutlast (predD p q) xs = allbutlast p xs && allbutlast (predC q) xs.
Lemma allbutlast_predT (xs: seq X): allbutlast predT xs.
Lemma eq_allbutlast xs: p =1 q → allbutlast p xs = allbutlast q xs.
Lemma allbutlast_take xs n: allbutlast p xs → allbutlast p (take n xs).
Lemma allbutlast_drop xs n: allbutlast p xs → allbutlast p (drop n xs).
End AllButLast.
Section TransitiveClosure.
Variable char: finType.
Variable A: dfa char.
Definition nPlus rs := foldr (@Plus char) (Void _) rs.
Lemma mem_nPlus (rs: seq _) w:
reflect (exists2 r: regular_expression char, r \in rs & w \in r)
(w \in nPlus rs).
Definition dfa_step_any x y := enum ( [pred a | dfa_step A x a == y] ).
Lemma dfa_step_anyP x y a:
reflect (dfa_step A x a = y)
(a \in dfa_step_any x y).
Definition R0 x y := let r := nPlus (map (@Atom _) (dfa_step_any x y)) in
if x == y then Plus r (Eps _) else r.
Lemma mem_R0 w x y:
reflect (w = [::] ∧ x=y ∨ exists2 a, w = [::a] & dfa_step A x a = y)
(w \in R0 x y).
Function R (X: {set A}) (x y: A) {measure [fun X ⇒ #|X|] X} :=
match [pick z in X] with
| None ⇒ R0 x y
| Some z ⇒ let X' := X :\ z in
Plus (Conc (R X' x z) (Conc (Star (R X' z z)) (R X' z y))) (R X' x y)
end.
Functional Scheme R_ind := Induction for R Sort Prop.
Notation "'R^' X" := (R X) (at level 8).
Definition L (X: {set A}) (x y: A) :=
[pred w | (last x (dfa_run' A x w) == y)
&& allbutlast (mem X) (dfa_run' A x w) ].
Notation "'L^' X" := (L X) (at level 8).
Lemma LP (X: {set A}) (x y: A) w:
reflect (last x (dfa_run' A x w) = y ∧ allbutlast (mem X) (dfa_run' A x w))
(w \in L^X x y).
Lemma L_monotone (X: {set A}) (x y z: A): {subset L^X x y ≤ L^(z |: X) x y}.
Lemma L_nil X x y: reflect (x = y) ([::] \in L^X x y).
Lemma setC1_pred1 (T: finType) (z: T): mem [set¬ z] =1 predC (pred1 z).
Lemma run_split x z w: z \in dfa_run' A x w →
∃ w1, ∃ w2,
w = w1++w2 ∧
size w2 < size w ∧
z \notin belast (dfa_run' A x w1) ∧
last x (dfa_run' A x w1) = z.
Lemma L_split X x y z w:
w \in L^(z |: X) x y →
w \in L^X x y ∨
∃ w1, ∃ w2,
w = w1 ++ w2 ∧
size w2 < size w ∧
w1 \in L^X x z ∧
w2 \in L^(z |: X) z y.
Lemma L_cat (X: {set A}) x y z w1 w2:
z \in X →
w1 \in L^X x z →
w2 \in L^X z y →
w1++w2 \in L^X x y.
Lemma L_catL X x y z w1 w2:
w1 \in L^X x z →
w2 \in L^(z |: X) z y →
w1++w2 \in L^(z |: X) x y.
Lemma L_catR X x y z w1 w2:
w1 \in L^(z |: X) x z →
w2 \in L^X z y →
w1++w2 \in L^(z |: X) x y.
Lemma L_flatten (X: {set A}) z vv: all (L^X z z) vv →
flatten vv \in L^(z |: X) z z.
(*
Lemma L_rec (X: {set A}) x y z:
L^(z |: X) x y =i plus (conc (L^X x z) (conc (star (L^X z z)) (L^X z y)))
(L^X x y).
Proof.
move => w.
apply/idP/idP.
apply/(size_induction size): w x y. w IHw x y.
destruct w.
move => Hw. apply/plusP. by right.
move/L_split => [/LP [H1 H2]|[w1 [w2 [Hw' [H1 [Hw1 Hw2]]]]]].
apply/plusP. right. by apply/LP.
move: (IHw w2 H1 z y Hw2) Hw' => H4 ->. clear IHw H1.
apply/plusP. left.
apply/concP. exists w1 => //. exists w2 => //.
apply/concP.
move/plusP: H4 => [].
move/concP => [w3 Hw3] [w4].
move/concP => [w5 Hw5] [w6 Hw6].
move => Hw4 Hw2'. subst.
ecase (@nilP _ w3) => [->|/eqP Hw3nil].
exists w5 => //. by exists w6 => //.
exists (w3++w5).
apply/starP. move/starP: Hw5 => [] vv Hvv ->.
exists (w3::vv); last by done.
by rewrite /= in_simpl /= Hw3nil /= Hw3.
rewrite catA. by eauto.
move => Hw2'.
exists [::] => //.
by exists w2 => //.
move/plusP => []; last exact: L_monotone.
move/concP => [w1 Hw1] [w2].
move/concP => [w3 /starP [vv Hvv Hvvf]] [w4 Hw4] Hw2' Hw.
subst.
apply: L_catL => //.
apply: L_catR => //.
move: Hvv. rewrite all_predD => /andP [H0 H1].
by apply: L_flatten.
Qed.
*)
Lemma conc_eq (l1: language char) l2 l3 l4: l1 =i l2 → l3 =i l4 → conc l1 l3 =i conc l2 l4.
Lemma star_eq (l1: language char) l2: l1 =i l2 → star l1 =i star l2.
Lemma orbr2 a b c: a = b → a || c = b || c.
(*
Lemma L_R n (X: {set A}) x y: $|X| = n -> L^X x y =i R^X x y.
Proof.
elim: n X x y => [|n IHn] X x y.
move/cards0_eq => ->.
rewrite R_equation.
case: pickP => [z|Hset0 w];
first by rewrite in_set0.
apply/LP/mem_R0.
move => [] H.
move/(allbutlast_pred0 Hset0).
destruct w; try destruct w => //;
by eauto.
move => [[-> ->]|[a [-> <-]]]; last by done.
apply/LP. by apply/L_nil.
move => HX w.
rewrite R_equation.
case: pickP => [z Hz|Hset0].
have HsizeX: ($|X :\ z| = n).
move: HX. rewrite (cardsD1 z) Hz add1n.
by move => [].
rewrite -(setD1K Hz).
rewrite (L_rec _ _) -2!topredE /= /plus /= setD1K => //.
rewrite !IHn => //.
apply: orbr2.
apply: conc_eq.
move => v.
exact: IHn.
apply: conc_eq.
apply: star_eq.
exact: IHn.
exact: IHn.
have: (X = set0).
apply/setP.
move => v.
by rewrite Hset0 in_set0.
move/eqP.
by rewrite -cards_eq0 HX.
Qed.
*)
Lemma dfa_L x y: L^setT x y =i [pred w | last x (dfa_run' A x w) == y ].
Definition dfa_to_re: regular_expression char :=
nPlus (map (R^setT (dfa_s A)) (enum (dfa_fin A))).
(*
Lemma dfa_to_re_correct: dfa_lang A =i dfa_to_re.
Proof.
move => w.
apply/idP/idP.
rewrite /= -dfa_run_accept => H.
apply/mem_nPlus.
exists (R^setT (dfa_s A) (last (dfa_s A) (dfa_run' A (dfa_s A) w))).
apply/mapP.
exists (last (dfa_s A) (dfa_run' A (dfa_s A) w)) => //.
by rewrite mem_enum.
rewrite <- (@L_R $|A|).
by rewrite dfa_L in_simpl.
by rewrite cardsE.
move/mem_nPlus => [r].
move/mapP => [] f.
rewrite mem_enum.
move => H0 => ->. rewrite <- (@L_R $|A|).
by rewrite dfa_L in_simpl -dfa_run_accept => /eqP ->.
by rewrite cardsE.
Qed.
*)
Lemma nPlus_standard rs: all (standard char) rs → standard char (nPlus rs).
Lemma R_standard' n (X: {set A}) x y: #|X| = n → standard char (R^X x y).
Lemma R_standard (X: {set A}) x y: standard char (R^X x y).
Lemma dfa_to_re_standard: standard char dfa_to_re.
End TransitiveClosure.
Section Ext_Standard.
Variable char: finType.
Definition ext_re_to_std_re (r: regular_expression char) := dfa_to_re (re_to_dfa r).
Lemma ext_re_to_std_re_standard r: standard char (ext_re_to_std_re r).
(*
Lemma ext_re_to_std_re_correct r: (ext_re_to_std_re r) =i r.
Proof.
move => w.
by rewrite /ext_re_to_std_re -dfa_to_re_correct re_to_dfa_correct.
Qed.
*)
End Ext_Standard.
Require Import automata misc regexp re_standard re_fa.
Set Implicit Arguments.
Import Prenex Implicits.
Import Automata.
Lemma set1UrP (T: finType) (X: {set T}) x: reflect (x |: X = X) (x \in X).
Lemma plusP {char} r s (w: word char):
reflect (w \in r ∨ w \in s)
(w \in plus r s).
Lemma set_pick_size {F: finType} (X: {set F}) z: [pick z in X] = Some z → #|X :\ z| < #|X|.
Lemma setU1_predI {F: finType} (X: {set F}) z: (z \notin X) → (mem X) =1 predI (mem (z |: X)) (predC (pred1 z)).
Lemma all_predD {X} (q p: pred X) xs: all (predD q p) xs = all q xs && all (predC p) xs.
Section AllButLastDef.
Variable X: Type.
Variable p: pred X.
Fixpoint belast (xs: seq X) :=
match xs with
| [::] ⇒ [::]
| [::x] ⇒ [::]
| x::xs ⇒ x::(belast xs)
end.
Lemma belast_rcons (x: X) xs:
belast (rcons xs x) = xs.
Definition allbutlast xs := all p (belast xs).
End AllButLastDef.
Implicit Arguments allbutlast [X].
Section AllButLast.
Variable X: Type.
Variable p q: pred X.
(* p => q -> allbutlast p -> allbutlast q *)
Lemma allbutlast_impl xs:
subpred p q →
allbutlast p xs →
allbutlast q xs.
Lemma allbutlast_nil: allbutlast p [::] = true.
Lemma allbutlast_cons x xs: p x → allbutlast p xs → allbutlast p (x::xs).
(* if at least one element in xs is actually
applied to p we can extract that application. *)
Lemma allbutlast_cons' x y xs: allbutlast p (x::y::xs) → p x && allbutlast p (y::xs).
(* if p holds everywhere on xs, it also holds
for all but the last element *)
Lemma all_allbutlast xs: all p xs → allbutlast p xs.
(* we can either extract an application of p x or
x is the last element in x::xs (i.e. xs is empty). *)
Lemma allbutlast_cons'' x (xs: seq X): allbutlast p (x::xs) → (size xs == 0) || (p x && allbutlast p xs).
(* all .. + allbutlast .. -> allbutlast (.. + ..) *)
Lemma all_allbutlast_cat xs ys: all p xs → allbutlast p ys → allbutlast p (xs++ys).
Lemma allbutlast_cat xs ys: allbutlast p (xs++ys) → allbutlast p xs ∧ allbutlast p ys.
(* with p (last xs) we can extend allbutlast to all. *)
Lemma allbutlast_last x xs: allbutlast p xs → p (last x xs) → all p xs.
(* constant false can only hold for one element or fewer. *)
Lemma allbutlast_pred0 xs: p =1 pred0 → allbutlast p xs → size xs ≤ 1.
Lemma allbutlast_predI xs: allbutlast (predI p q) xs = allbutlast p xs && allbutlast q xs.
Lemma allbutlast_predD xs: allbutlast (predD p q) xs = allbutlast p xs && allbutlast (predC q) xs.
Lemma allbutlast_predT (xs: seq X): allbutlast predT xs.
Lemma eq_allbutlast xs: p =1 q → allbutlast p xs = allbutlast q xs.
Lemma allbutlast_take xs n: allbutlast p xs → allbutlast p (take n xs).
Lemma allbutlast_drop xs n: allbutlast p xs → allbutlast p (drop n xs).
End AllButLast.
Section TransitiveClosure.
Variable char: finType.
Variable A: dfa char.
Definition nPlus rs := foldr (@Plus char) (Void _) rs.
Lemma mem_nPlus (rs: seq _) w:
reflect (exists2 r: regular_expression char, r \in rs & w \in r)
(w \in nPlus rs).
Definition dfa_step_any x y := enum ( [pred a | dfa_step A x a == y] ).
Lemma dfa_step_anyP x y a:
reflect (dfa_step A x a = y)
(a \in dfa_step_any x y).
Definition R0 x y := let r := nPlus (map (@Atom _) (dfa_step_any x y)) in
if x == y then Plus r (Eps _) else r.
Lemma mem_R0 w x y:
reflect (w = [::] ∧ x=y ∨ exists2 a, w = [::a] & dfa_step A x a = y)
(w \in R0 x y).
Function R (X: {set A}) (x y: A) {measure [fun X ⇒ #|X|] X} :=
match [pick z in X] with
| None ⇒ R0 x y
| Some z ⇒ let X' := X :\ z in
Plus (Conc (R X' x z) (Conc (Star (R X' z z)) (R X' z y))) (R X' x y)
end.
Functional Scheme R_ind := Induction for R Sort Prop.
Notation "'R^' X" := (R X) (at level 8).
Definition L (X: {set A}) (x y: A) :=
[pred w | (last x (dfa_run' A x w) == y)
&& allbutlast (mem X) (dfa_run' A x w) ].
Notation "'L^' X" := (L X) (at level 8).
Lemma LP (X: {set A}) (x y: A) w:
reflect (last x (dfa_run' A x w) = y ∧ allbutlast (mem X) (dfa_run' A x w))
(w \in L^X x y).
Lemma L_monotone (X: {set A}) (x y z: A): {subset L^X x y ≤ L^(z |: X) x y}.
Lemma L_nil X x y: reflect (x = y) ([::] \in L^X x y).
Lemma setC1_pred1 (T: finType) (z: T): mem [set¬ z] =1 predC (pred1 z).
Lemma run_split x z w: z \in dfa_run' A x w →
∃ w1, ∃ w2,
w = w1++w2 ∧
size w2 < size w ∧
z \notin belast (dfa_run' A x w1) ∧
last x (dfa_run' A x w1) = z.
Lemma L_split X x y z w:
w \in L^(z |: X) x y →
w \in L^X x y ∨
∃ w1, ∃ w2,
w = w1 ++ w2 ∧
size w2 < size w ∧
w1 \in L^X x z ∧
w2 \in L^(z |: X) z y.
Lemma L_cat (X: {set A}) x y z w1 w2:
z \in X →
w1 \in L^X x z →
w2 \in L^X z y →
w1++w2 \in L^X x y.
Lemma L_catL X x y z w1 w2:
w1 \in L^X x z →
w2 \in L^(z |: X) z y →
w1++w2 \in L^(z |: X) x y.
Lemma L_catR X x y z w1 w2:
w1 \in L^(z |: X) x z →
w2 \in L^X z y →
w1++w2 \in L^(z |: X) x y.
Lemma L_flatten (X: {set A}) z vv: all (L^X z z) vv →
flatten vv \in L^(z |: X) z z.
(*
Lemma L_rec (X: {set A}) x y z:
L^(z |: X) x y =i plus (conc (L^X x z) (conc (star (L^X z z)) (L^X z y)))
(L^X x y).
Proof.
move => w.
apply/idP/idP.
apply/(size_induction size): w x y. w IHw x y.
destruct w.
move => Hw. apply/plusP. by right.
move/L_split => [/LP [H1 H2]|[w1 [w2 [Hw' [H1 [Hw1 Hw2]]]]]].
apply/plusP. right. by apply/LP.
move: (IHw w2 H1 z y Hw2) Hw' => H4 ->. clear IHw H1.
apply/plusP. left.
apply/concP. exists w1 => //. exists w2 => //.
apply/concP.
move/plusP: H4 => [].
move/concP => [w3 Hw3] [w4].
move/concP => [w5 Hw5] [w6 Hw6].
move => Hw4 Hw2'. subst.
ecase (@nilP _ w3) => [->|/eqP Hw3nil].
exists w5 => //. by exists w6 => //.
exists (w3++w5).
apply/starP. move/starP: Hw5 => [] vv Hvv ->.
exists (w3::vv); last by done.
by rewrite /= in_simpl /= Hw3nil /= Hw3.
rewrite catA. by eauto.
move => Hw2'.
exists [::] => //.
by exists w2 => //.
move/plusP => []; last exact: L_monotone.
move/concP => [w1 Hw1] [w2].
move/concP => [w3 /starP [vv Hvv Hvvf]] [w4 Hw4] Hw2' Hw.
subst.
apply: L_catL => //.
apply: L_catR => //.
move: Hvv. rewrite all_predD => /andP [H0 H1].
by apply: L_flatten.
Qed.
*)
Lemma conc_eq (l1: language char) l2 l3 l4: l1 =i l2 → l3 =i l4 → conc l1 l3 =i conc l2 l4.
Lemma star_eq (l1: language char) l2: l1 =i l2 → star l1 =i star l2.
Lemma orbr2 a b c: a = b → a || c = b || c.
(*
Lemma L_R n (X: {set A}) x y: $|X| = n -> L^X x y =i R^X x y.
Proof.
elim: n X x y => [|n IHn] X x y.
move/cards0_eq => ->.
rewrite R_equation.
case: pickP => [z|Hset0 w];
first by rewrite in_set0.
apply/LP/mem_R0.
move => [] H.
move/(allbutlast_pred0 Hset0).
destruct w; try destruct w => //;
by eauto.
move => [[-> ->]|[a [-> <-]]]; last by done.
apply/LP. by apply/L_nil.
move => HX w.
rewrite R_equation.
case: pickP => [z Hz|Hset0].
have HsizeX: ($|X :\ z| = n).
move: HX. rewrite (cardsD1 z) Hz add1n.
by move => [].
rewrite -(setD1K Hz).
rewrite (L_rec _ _) -2!topredE /= /plus /= setD1K => //.
rewrite !IHn => //.
apply: orbr2.
apply: conc_eq.
move => v.
exact: IHn.
apply: conc_eq.
apply: star_eq.
exact: IHn.
exact: IHn.
have: (X = set0).
apply/setP.
move => v.
by rewrite Hset0 in_set0.
move/eqP.
by rewrite -cards_eq0 HX.
Qed.
*)
Lemma dfa_L x y: L^setT x y =i [pred w | last x (dfa_run' A x w) == y ].
Definition dfa_to_re: regular_expression char :=
nPlus (map (R^setT (dfa_s A)) (enum (dfa_fin A))).
(*
Lemma dfa_to_re_correct: dfa_lang A =i dfa_to_re.
Proof.
move => w.
apply/idP/idP.
rewrite /= -dfa_run_accept => H.
apply/mem_nPlus.
exists (R^setT (dfa_s A) (last (dfa_s A) (dfa_run' A (dfa_s A) w))).
apply/mapP.
exists (last (dfa_s A) (dfa_run' A (dfa_s A) w)) => //.
by rewrite mem_enum.
rewrite <- (@L_R $|A|).
by rewrite dfa_L in_simpl.
by rewrite cardsE.
move/mem_nPlus => [r].
move/mapP => [] f.
rewrite mem_enum.
move => H0 => ->. rewrite <- (@L_R $|A|).
by rewrite dfa_L in_simpl -dfa_run_accept => /eqP ->.
by rewrite cardsE.
Qed.
*)
Lemma nPlus_standard rs: all (standard char) rs → standard char (nPlus rs).
Lemma R_standard' n (X: {set A}) x y: #|X| = n → standard char (R^X x y).
Lemma R_standard (X: {set A}) x y: standard char (R^X x y).
Lemma dfa_to_re_standard: standard char dfa_to_re.
End TransitiveClosure.
Section Ext_Standard.
Variable char: finType.
Definition ext_re_to_std_re (r: regular_expression char) := dfa_to_re (re_to_dfa r).
Lemma ext_re_to_std_re_standard r: standard char (ext_re_to_std_re r).
(*
Lemma ext_re_to_std_re_correct r: (ext_re_to_std_re r) =i r.
Proof.
move => w.
by rewrite /ext_re_to_std_re -dfa_to_re_correct re_to_dfa_correct.
Qed.
*)
End Ext_Standard.