Library RegLang.wmso
From mathcomp Require Import all_ssreflect.
Require Import misc languages dfa nfa regexp.
Set Implicit Arguments.
Unset Printing Implicit Defensive.
Unset Strict Implicit.
Require Import misc languages dfa nfa regexp.
Set Implicit Arguments.
Unset Printing Implicit Defensive.
Unset Strict Implicit.
Preliminaries
Lemma behead_cons (T:Type) n (t : n.-tuple T) a : behead_tuple (cons_tuple a t) = t.
Proof.
rewrite /cons_tuple /behead_tuple /=.
case: t => t tP /=. set X := (behead_tupleP _). by rewrite (eq_irrelevance X tP).
Qed.
Weak Monadic Second-Order Logic
All variables are interpreted as finite sets (actually lists) of natural numbers
Definition valuation := nat -> seq nat.
Implicit Types (s t : form) (X Y : nat) (I : valuation) (N : seq nat).
Definition cons N I : valuation := fun k => if k is k'.+1 then I k' else N.
Fixpoint satisfies (I : valuation) (s : form) :=
match s with
| Incl X Y => {subset I X <= I Y}
| Less X Y => forall x y, x \in I X -> y \in I Y -> x < y
| FF => False
| Imp s t => satisfies I s -> satisfies I t
| Ex s => exists N, satisfies (cons N I) s
end.
Fixpoint bound (s : form) : nat :=
match s with
| Incl X Y => maxn X.+1 Y.+1
| Less X Y => maxn X.+1 Y.+1
| FF => 0
| Imp s t => maxn (bound s) (bound t)
| Ex s => (bound s).-1
end.
Definition agree n I I' := forall X, X < n -> I X =i I' X.
Lemma agree_dc n m I I' : n <= m -> agree m I I' -> agree n I I'.
Proof. move => A B X ltn_m. apply: B. exact: leq_trans A. Qed.
Lemma coincidence I I' s:
agree (bound s) I I' -> satisfies I s <-> satisfies I' s.
Proof.
elim: s I I' => [X Y|X Y||s IHs t IHt|s IHs] /= I I' C.
- split.
+ move => A B. rewrite -!C ?leq_maxl ?leq_maxr //. exact: A.
+ move => A B. rewrite !C ?leq_maxl ?leq_maxr //. exact: A.
- split => H x y;[rewrite -!C|rewrite !C]; try solve [exact: H|by rewrite ?leq_maxl ?leq_maxr].
- tauto.
- by rewrite -(IHs I I') ?(IHt I I') //; apply: agree_dc C; rewrite ?leq_maxl ?leq_maxr.
- have bound_s N : agree (bound s) (cons N I) (cons N I').
{ move => X. case: X C => //= Y A B. apply: A. rewrite -ltnS. by case: (bound s) B. }
split.
+ move => [N] sat_s. exists N. rewrite -IHs. eassumption. exact: bound_s.
+ move => [N] sat_s. exists N. rewrite IHs. eassumption. exact: bound_s.
Qed.
Lemma weak_coincidence I I' s : (forall X, I X =i I' X) -> satisfies I s -> satisfies I' s.
Proof. move => H. by rewrite (@coincidence I I' s). Qed.
Implicit Types (s t : form) (X Y : nat) (I : valuation) (N : seq nat).
Definition cons N I : valuation := fun k => if k is k'.+1 then I k' else N.
Fixpoint satisfies (I : valuation) (s : form) :=
match s with
| Incl X Y => {subset I X <= I Y}
| Less X Y => forall x y, x \in I X -> y \in I Y -> x < y
| FF => False
| Imp s t => satisfies I s -> satisfies I t
| Ex s => exists N, satisfies (cons N I) s
end.
Fixpoint bound (s : form) : nat :=
match s with
| Incl X Y => maxn X.+1 Y.+1
| Less X Y => maxn X.+1 Y.+1
| FF => 0
| Imp s t => maxn (bound s) (bound t)
| Ex s => (bound s).-1
end.
Definition agree n I I' := forall X, X < n -> I X =i I' X.
Lemma agree_dc n m I I' : n <= m -> agree m I I' -> agree n I I'.
Proof. move => A B X ltn_m. apply: B. exact: leq_trans A. Qed.
Lemma coincidence I I' s:
agree (bound s) I I' -> satisfies I s <-> satisfies I' s.
Proof.
elim: s I I' => [X Y|X Y||s IHs t IHt|s IHs] /= I I' C.
- split.
+ move => A B. rewrite -!C ?leq_maxl ?leq_maxr //. exact: A.
+ move => A B. rewrite !C ?leq_maxl ?leq_maxr //. exact: A.
- split => H x y;[rewrite -!C|rewrite !C]; try solve [exact: H|by rewrite ?leq_maxl ?leq_maxr].
- tauto.
- by rewrite -(IHs I I') ?(IHt I I') //; apply: agree_dc C; rewrite ?leq_maxl ?leq_maxr.
- have bound_s N : agree (bound s) (cons N I) (cons N I').
{ move => X. case: X C => //= Y A B. apply: A. rewrite -ltnS. by case: (bound s) B. }
split.
+ move => [N] sat_s. exists N. rewrite -IHs. eassumption. exact: bound_s.
+ move => [N] sat_s. exists N. rewrite IHs. eassumption. exact: bound_s.
Qed.
Lemma weak_coincidence I I' s : (forall X, I X =i I' X) -> satisfies I s -> satisfies I' s.
Proof. move => H. by rewrite (@coincidence I I' s). Qed.
Section Language.
Variables (char : finType).
Definition I_of n (v : seq (n.-tuple bool)) : valuation :=
fun X => [seq i <- iota 0 (size v) | nth false (nth [tuple of nseq n false] v i) X].
Definition vec_of (w : word char) : seq (#|char|.-tuple bool) :=
map (fun a => [tuple X == enum_rank a | X < #|char|]) w.
Lemma I_of_vev_max k (a:char) w:
k \in I_of (vec_of w) (enum_rank a) -> k < size w.
Proof. by rewrite /vec_of /I_of mem_filter mem_iota add0n size_map => /andP[_]. Qed.
Lemma I_of_vecP k a w: k < size w ->
(k \in I_of (vec_of w) (enum_rank a) = (nth a w k == a)).
Proof.
move => H. rewrite /vec_of /I_of mem_filter mem_iota add0n size_map /=.
rewrite (nth_map a) // H andbT.
rewrite (nth_map (enum_rank a)) ?size_tuple ?ltn_ord //.
by rewrite nth_ord_enum (inj_eq enum_rank_inj) eq_sym.
Qed.
Definition vec_lang n s := fun v : seq (n.-tuple bool) => satisfies (I_of v) s.
Definition mso_lang s := fun w => vec_lang s (vec_of w).
Lemma vec_of_hom : homomorphism vec_of.
Proof. exact: map_cat. Qed.
Lemma mso_preim s : mso_lang s =p preimage vec_of (@vec_lang #|char| s).
Proof. done. Qed.
End Language.
Notation vec n := [finType of n.-tuple bool].
Definition nfa_for_bot n := dfa_to_nfa (dfa_void (vec n)).
Definition nfa_for_imp n (A B : nfa (vec n)) :=
dfa_to_nfa (dfa_op implb (nfa_to_dfa A) (nfa_to_dfa B)).
MSO Primitives
Definition nfa_for_incl n X Y :=
{| nfa_state := [finType of unit];
nfa_s := setT;
nfa_fin := setT;
nfa_trans := fun p (v : vec n) q => nth false v X ==> nth false v Y |}.
Definition enfa_for_ltn n X Y : enfa (vec n) :=
{| enfa_s := [set false];
enfa_f := setT;
enfa_trans := fun (c : option (vec n)) p q =>
match p,c,q with
| false, Some a, false => ~~ nth false a Y
| true, Some a, true => ~~ nth false a X
| false, None, true => true
| _,_,_ => false
end; |}.
Definition nfa_for_ltn n X Y := nfa_of (enfa_for_ltn n X Y).
Existential Quantification
Definition prj0 n (w : seq (vec n.+1)) : seq (vec n) :=
map (fun v : vec (n.+1) => [tuple of behead v]) w.
Prenex Implicits prj0.
Definition trans_b0 n (A : nfa (vec n.+1)) (p q : A) :=
[exists b, nfa_trans p [tuple of b :: nseq n false] q].
Arguments trans_b0 [n] A p q.
Definition nfa_for_ex n (A : nfa (vec n.+1)) : nfa (vec n) :=
{| nfa_s := nfa_s A;
nfa_fin := [set p | [exists (q | q \in nfa_fin A), connect (trans_b0 A) p q]];
nfa_trans := fun p (v : vec n) q => [exists b, nfa_trans p [tuple of b::v] q] |}.
Translation to NFAs
Fixpoint nfa_of_form n s {struct s} : nfa (vec n) :=
match s with
| Incl X Y => nfa_for_incl n X Y
| Less X Y => nfa_for_ltn n X Y
| FF => nfa_for_bot n
| Imp s t => nfa_for_imp (nfa_of_form n s) (nfa_of_form n t)
| Ex s => nfa_for_ex (nfa_of_form n.+1 s)
end.
Fixpoint glue (bs : seq bool) n (w : seq (vec n)) :=
match bs,w with
| b::bs,v::w => [tuple of b :: v] :: glue bs w
| b::bs,[::] => [tuple of b :: nseq n false] :: glue bs [::]
| nil,w => map (fun v : vec n => [tuple of false :: v]) w
end.
Lemma nfa_for_exI n (A : nfa (vec n.+1)) b w :
glue b w \in nfa_lang A -> w \in nfa_lang (nfa_for_ex A).
Proof.
rewrite /nfa_lang !inE.
case/exists_inP => s s1 s2. apply/exists_inP. exists s => //.
elim: b w s {s1} s2 => [w p /=|b bs IH w p].
- elim: w p => /= [|v w IHw] p.
+ rewrite /= inE => H. by apply/exists_inP; exists p.
+ apply: sub_exists => q /andP [q1 q2]. rewrite IHw // andbT.
by apply/existsP;exists false.
- case: w => [|v w] /=.
+ case/exists_inP => q q1 /IH /= q2. rewrite !inE in q2 *.
apply: sub_exists q2 => r /andP [r1 r2].
rewrite r1 (connect_trans (connect1 _) r2) // /trans_b0. by apply/existsP;exists b.
+ apply: sub_exists => q /andP [q1 q2]. rewrite IH // andbT. by apply/existsP;exists b.
Qed.
Lemma nfa_for_exE n (A : nfa (vec n.+1)) w :
w \in nfa_lang (nfa_for_ex A) -> exists b : seq bool, glue b w \in nfa_lang A.
Proof.
rewrite /nfa_lang /= !inE => H.
suff S (q:A) : @nfa_accept _ (nfa_for_ex A) q w -> exists b, nfa_accept q (glue b w).
{ case/exists_inP : H => p p1 /S [b b1]. exists b. rewrite inE. by apply/exists_inP; exists p. }
elim: w q {H} => [|v vs IH] q /=.
- rewrite inE => /exists_inP [f f1 /connectP[p]].
elim: p q => [x _ |p ps IHp q /= /andP [pth1 pth2]] /= E; first by exists nil; subst.
case: (IHp _ pth2 E) => bs Hbs. case/existsP : pth1 => b pth1. exists (b::bs).
by apply/exists_inP; exists p.
- case/exists_inP => p /= /existsP [b p1] p2. case: (IH _ p2) => bs Hbs. exists (b::bs).
by apply/exists_inP; exists p.
Qed.
Lemma size_glue b n (v : seq (vec n)) : size (glue b v) = maxn (size b) (size v).
Proof.
elim: b v => [|b bs IH] v /=; first by rewrite max0n size_map.
case: v => [|v vs]; by rewrite /= ?maxnSS IH ?maxn0.
Qed.
Lemma nth_glue0 b n (v : seq (vec n)) k :
nth false (nth [tuple of nseq n.+1 false] (glue b v) k) 0 =
nth false b k.
Proof.
elim: k v b => [|k IH] [|v vs] [|b bs] //; rewrite [glue _ _]/= ?nth_nil ?nth_cons ?IH //.
case: (ltnP k (size vs)) => A.
- by rewrite (nth_map [tuple of nseq n false]) //.
- by rewrite [_ _ _ k]nth_default // size_map.
Qed.
Lemma I_of_glue0 i b n (v : seq (vec n)) :
i \in I_of (glue b v) 0 = nth false b i.
Proof.
rewrite mem_filter mem_iota add0n leq0n andTb.
rewrite nth_glue0 size_glue leq_max andbC.
case: (ltnP i (size b)) => //= A. by rewrite nth_default ?andbF.
Qed.
Lemma nth_glueS b n (v : seq (vec n)) i k :
nth false (nth [tuple of nseq n.+1 false] (glue b v) k) i.+1 =
nth false (nth [tuple of nseq n false] v k) i.
Proof.
elim: k v b => [|k IH] [|v vs] [|b bs] //.
- by rewrite [glue _ _]/= IH !nth_nil nth_nseq if_same.
- rewrite [glue _ _]/= !nth_cons.
case: (ltnP k (size vs)) => A.
+ by rewrite (nth_map [tuple of nseq n false]).
+ by rewrite ![_ _ _ k]nth_default ?size_map.
- by rewrite [glue _ _]/= !nth_cons.
Qed.
Lemma I_of_glueS i b n (v : seq (vec n)) k :
i \in I_of (glue b v) k.+1 = nth false (nth [tuple of nseq n false] v i) k.
Proof.
rewrite mem_filter mem_iota add0n leq0n andTb.
rewrite nth_glueS size_glue leq_max andbC orbC.
case: (ltnP i (size v)) => //= A.
by rewrite [_ _ v i]nth_default // nth_nseq if_same andbF.
Qed.
Lemma vec_ex_glue s n (vs : seq (vec n)) :
vec_lang (Ex s) vs -> exists bs, vec_lang s (glue bs vs).
Proof.
rewrite /vec_lang /= => [[N sat_s]].
exists [seq i \in N | i <- iota 0 (\max_(k <- N) k).+1].
apply: weak_coincidence sat_s => X i.
case: X => [|X].
- rewrite I_of_glue0. case: (boolP (i < (\max_(k <- N) k).+1)) => ltn_max.
+ by rewrite (nth_map 0) ?size_iota // nth_iota.
+ rewrite nth_default ?size_map ?size_iota 1?leqNgt //.
apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_seq_sup H _ _.
- rewrite I_of_glueS /= /I_of mem_filter mem_iota /= add0n.
case: (ltnP i (size vs)) => H; first by rewrite andbT.
rewrite andbF [nth _ _ i]nth_default //.
by rewrite nth_nseq if_same.
Qed.
Lemma vec_lang0 s n (v : seq (vec n)) k :
vec_lang s v <-> vec_lang s (v ++ nseq k [tuple of nseq n false]).
Proof.
apply coincidence => X ? i. rewrite !mem_filter !mem_iota /= !add0n size_cat nth_cat.
case: (boolP (i < size v)) => Hi; first by rewrite ltn_addr.
by rewrite andbF !(nth_nseq,if_same).
Qed.
Lemma prj_glue bs n (v : seq (vec n)) :
exists k, prj0 (glue bs v) = v ++ nseq k [tuple of nseq n false].
Proof.
exists (size bs - size v). elim: bs v => [|b bs IH] v /=.
- rewrite /prj0 -map_comp cats0 map_id_in //= => b. by rewrite !tupleE behead_cons.
- case: v => [| v vs] /=; by rewrite IH /= ?subn0 ?subss !tupleE behead_cons.
Qed.
Lemma vec_Ex_prj0 s n (w : word (vec n.+1)) : vec_lang s w -> vec_lang (Ex s) (prj0 w).
Proof.
rewrite /vec_lang => /= A.
exists [seq i <- iota 0 (size w) | nth false (nth [tuple of nseq n.+1 false] w i) 0].
apply: weak_coincidence A => X i. rewrite mem_filter mem_iota add0n /= /cons.
case: X => [|X].
+ by rewrite mem_filter mem_iota /= add0n.
+ rewrite mem_filter mem_iota add0n size_map /prj0 andTb -nth_behead.
(case: (boolP (i < _)); rewrite ?andbF ?andbT //) => A. congr nth.
by erewrite nth_map.
Qed.
Lemma nfa_for_ex_correct n s (A : nfa (vec n.+1)) v:
(forall u, reflect (vec_lang s u) (u \in nfa_lang A)) ->
reflect (vec_lang (Ex s) v) (v \in nfa_lang (nfa_for_ex A)).
Proof.
move => IHs. apply: (iffP idP).
+ case/nfa_for_exE => b. move/IHs. move/vec_Ex_prj0.
case: (prj_glue b v) => k ->. by rewrite -vec_lang0.
+ case/vec_ex_glue => b. move/IHs. exact: nfa_for_exI.
Qed.
Correctness of the NFAs for the primitive operations
Lemma nfa_for_incl_correct X Y n (v : seq (vec n)):
reflect (vec_lang (Incl X Y) v) (v \in nfa_lang (nfa_for_incl n X Y)).
Proof.
rewrite /nfa_lang inE. apply: (equivP existsP).
rewrite (_ : (exists _,_) <-> nfa_accept (tt : nfa_for_incl n X Y) v); last first.
- split => [[x]|];[case: x|exists tt]; by rewrite inE.
- rewrite (_ : vec_lang _ _ <-> (forall u, u \in v -> nth false u X -> nth false u Y)).
+ elim: v => //= v vs IH. split.
* case/exists_inP => [[/implyP A] /IH B] u /predU1P []; first by move=>?;subst.
exact: B.
* move => A. apply/exists_inP; exists tt;[apply/implyP|].
-- apply: A; exact: mem_head.
-- apply/IH => u Hu. apply: A. by rewrite inE Hu orbT.
+ rewrite /vec_lang /=. split.
* move => A u in_v u_X.
set i := index u v.
move: (A i). rewrite /I_of !mem_filter !mem_iota !add0n /=.
rewrite index_mem in_v !andbT. rewrite nth_index //. by apply.
* move => A => k. rewrite /I_of !mem_filter !mem_iota !add0n /=.
case: (boolP (_ < _)); rewrite ?andbT ?andbF // => B.
set u := nth [tuple of nseq n false] v k.
apply A. by rewrite mem_nth.
Qed.
Definition zero_at n X := forall (v : vec n), nth false v X = false.
Lemma nfa_for_ltnP {X Y n} {v : seq (vec n)} :
reflect (exists v1 v2, [/\ v = v1 ++ v2, {in v1,zero_at n Y} & {in v2,zero_at n X}])
(v \in nfa_lang (nfa_for_ltn n X Y)).
Proof.
move: v => v0. apply: (iffP (nfa_ofP _ _)).
- rewrite /enfa_lang => [[[|_]]]; first by rewrite inE.
suff S q v:
enfa_accept (N := enfa_for_ltn n X Y) q v ->
if q
then {in v, zero_at n X}
else (exists v1 v2, [/\ v = v1 ++ v2, {in v1,zero_at n Y} & {in v2,zero_at n X}]).
{ by move/S. }
elim => // {v0 v} [||].
+ case => // _. by do 2 exists nil.
+ move => [|] a [|] //= v.
* move => A _ B u. case/predU1P => [->|]; by [rewrite (negbTE A)| apply: B].
* move => A _ [v1] [v2] [C D E].
exists (a :: v1); exists v2; split => //; first by rewrite C.
apply/all1s. split => //. by rewrite (negbTE A).
+ move => [|] [|] // v. by exists nil; exists v.
- move => [v1] [v2] [->] A B. exists false; first by rewrite inE.
elim: v1 A => /= [_|a v1 IH A].
+ (apply: EnfaNone; first instantiate (1 := true)) => //.
elim: v2 B {v0} => [_|a s IH B].
* constructor. by rewrite inE.
* (apply: EnfaSome; first instantiate (1 := true)) => //=.
-- by rewrite B ?inE ?eqxx.
-- apply: IH => u C. apply B. by rewrite inE C orbT.
+ apply: EnfaSome; first instantiate (1 := false).
* by rewrite /= A ?inE ?eqxx.
* apply IH => u C. apply A. by rewrite inE C orbT.
Qed.
Lemma mem_I_of n (v : seq (vec n)) X k :
(k \in I_of v X) = (k < size v) && nth false (nth [tuple of nseq n false] v k) X.
Proof. by rewrite mem_filter mem_iota add0n /= andbC. Qed.
Lemma nfa_for_ltn_correct X Y n (v : seq (vec n)):
reflect (vec_lang (Less X Y) v) (v \in nfa_lang (nfa_for_ltn n X Y)).
Proof.
apply: (iffP nfa_for_ltnP).
- move => [v1] [v2] [A B C] i j.
rewrite /I_of !mem_filter !mem_iota !add0n /= ![_ && (_ < _)]andbC.
case: (boolP (_ < _)) => //= D. case: (boolP (_ < _)) => //= E F G.
have Hi : i < size v1.
{ move: F. rewrite A nth_cat. case: (ifP _) => // /negbT H.
rewrite C ?mem_nth //. rewrite -leqNgt in H.
by rewrite -subSn // leq_subLR -size_cat -A. }
have : size v1 <= j.
{ move: G. rewrite A nth_cat. case: (ltnP j (size v1)) => // H.
by rewrite B ? mem_nth. }
exact: leq_trans.
- rewrite /vec_lang /= => A.
case: (boolP (has predT (I_of v X))).
+ case/hasP => x0 /max_mem k_in_X _.
set k := (\max_(i <- I_of v X) i) in k_in_X.
have size_k: k < size v by move: k_in_X; rewrite mem_I_of => /andP[].
have size_tk: size (take k.+1 v) = k.+1.
{ rewrite size_take.
case: (ltnP k.+1 (size v)) size_k => // H1 H2.
apply/eqP. by rewrite eqn_leq H1 H2. }
exists (take k.+1 v); exists (drop k.+1 v); split; first by rewrite cat_take_drop.
* move => u B. apply/negbTE/negP => D.
pose i := index u (take k.+1 v).
have E: i <= k by rewrite -ltnS -size_tk index_mem B.
move: (A k i). case/(_ _ _)/Wrap => //; last by rewrite leqNgt ltnS E.
rewrite mem_I_of (leq_ltn_trans E size_k) /=.
rewrite /i index_take // nth_index //. exact: mem_take B.
* move => u B. apply/negbTE/negP => D.
pose i := k.+1 + index u (drop k.+1 v).
have i_in_X : i \in I_of v X.
{ rewrite mem_I_of.
rewrite -[v](cat_take_drop k.+1) size_cat size_tk.
rewrite -addnS leq_add2l index_mem B andTb.
rewrite nth_cat size_tk leqNgt leq_addr /= /i.
by rewrite addnC -addnBA // subnn addn0 nth_index. }
have: i <= k by apply: bigmax_seq_sup i_in_X _ _.
by rewrite /i addSn -ltn_subRL subnn.
+ move/hasPn => /= B. exists nil; exists v; split => // u in_v.
apply/negbTE/negP => D.
pose i := index u v. move: (B i). case/(_ _)/Wrap => //.
by rewrite mem_I_of index_mem in_v nth_index.
Qed.
Theorem nfa_of_form_correct n (v : seq (n.-tuple bool)) s :
reflect (vec_lang s v) (v \in nfa_lang (nfa_of_form n s)).
Proof.
elim: s n v => [X Y|X Y||s IHs t IHt|s IHs] /= n v.
- exact: nfa_for_incl_correct.
- exact: nfa_for_ltn_correct.
- rewrite -dfa_to_nfa_correct in_simpl (negbTE (dfa_void_correct _ _)).
by constructor.
- rewrite -dfa_to_nfa_correct dfa_op_correct -!nfa_to_dfa_correct.
by apply: (iffP implyP) => A /IHs/A/IHt.
- exact: nfa_for_ex_correct.
Qed.
Greatest number used in first n variables
Definition lim I n := \max_(X < n) \max_(n <- I X) n.
Definition vec_of_val I n : seq (n.-tuple bool) :=
[seq [tuple i \in I X | X < n] | i <- iota 0 (lim I n).+1].
Lemma vec_of_val_agrees : forall I n, agree n I (I_of (vec_of_val I n)).
Proof.
move => I n X lt_n i.
rewrite mem_filter mem_iota /= add0n size_map size_iota.
case: (boolP (i < _)); rewrite ?(andbT,andbF) => A.
+ rewrite /vec_of_val.
rewrite (nth_map 0) ?size_iota // nth_iota // add0n.
by rewrite (nth_map (Ordinal lt_n)) ?size_enum_ord ?nth_enum_ord.
+ apply: contraNF A => A. rewrite ltnS. rewrite /lim.
apply: bigmax_sup => //. instantiate (1 := Ordinal lt_n) => /=.
exact: bigmax_seq_sup A _ _ .
Qed.
Lemma vec_of_valP I s : satisfies I s <-> satisfies (I_of (vec_of_val I (bound s))) s.
Proof. apply: coincidence. exact: vec_of_val_agrees. Qed.
Corollary satisfies_dec I s : decidable (satisfies I s).
Proof. apply: dec_iff (vec_of_valP I s). exact: decP (nfa_of_form_correct _ _). Qed.
Corollary mso_dec s : decidable (exists I, satisfies I s).
Proof.
pose n := bound s.
case: (nfa_inhabP (nfa_of_form n s)) => A;[left|right].
- case: A => w /(@nfa_of_form_correct n) Hw. by exists (I_of w).
- move => [I sat_I_s]. apply A.
exists (vec_of_val I n). apply/nfa_of_form_correct.
by rewrite /vec_lang -vec_of_valP.
Qed.
Corollary vec_lang_regular n s : regular (@vec_lang n s).
Proof.
apply/nfa_regular. exists (nfa_of_form n s) => x.
apply: rwP. exact: nfa_of_form_correct.
Qed.
Definition vec_of_val I n : seq (n.-tuple bool) :=
[seq [tuple i \in I X | X < n] | i <- iota 0 (lim I n).+1].
Lemma vec_of_val_agrees : forall I n, agree n I (I_of (vec_of_val I n)).
Proof.
move => I n X lt_n i.
rewrite mem_filter mem_iota /= add0n size_map size_iota.
case: (boolP (i < _)); rewrite ?(andbT,andbF) => A.
+ rewrite /vec_of_val.
rewrite (nth_map 0) ?size_iota // nth_iota // add0n.
by rewrite (nth_map (Ordinal lt_n)) ?size_enum_ord ?nth_enum_ord.
+ apply: contraNF A => A. rewrite ltnS. rewrite /lim.
apply: bigmax_sup => //. instantiate (1 := Ordinal lt_n) => /=.
exact: bigmax_seq_sup A _ _ .
Qed.
Lemma vec_of_valP I s : satisfies I s <-> satisfies (I_of (vec_of_val I (bound s))) s.
Proof. apply: coincidence. exact: vec_of_val_agrees. Qed.
Corollary satisfies_dec I s : decidable (satisfies I s).
Proof. apply: dec_iff (vec_of_valP I s). exact: decP (nfa_of_form_correct _ _). Qed.
Corollary mso_dec s : decidable (exists I, satisfies I s).
Proof.
pose n := bound s.
case: (nfa_inhabP (nfa_of_form n s)) => A;[left|right].
- case: A => w /(@nfa_of_form_correct n) Hw. by exists (I_of w).
- move => [I sat_I_s]. apply A.
exists (vec_of_val I n). apply/nfa_of_form_correct.
by rewrite /vec_lang -vec_of_valP.
Qed.
Corollary vec_lang_regular n s : regular (@vec_lang n s).
Proof.
apply/nfa_regular. exists (nfa_of_form n s) => x.
apply: rwP. exact: nfa_of_form_correct.
Qed.
Corollary mso_regular (char: finType) s : regular (@mso_lang char s).
Proof.
apply: regular_ext (mso_preim s).
exact: preim_regular (@vec_of_hom _) (vec_lang_regular _ _).
Qed.
Translation from NFAs to WMSO
Propositional Connectives
Lemma satNNPP I s : ~ ~ I |= s -> I |= s.
Proof. case: (satisfies_dec I s); tauto. Qed.
Notation "s --> t" := (Imp s t) (at level 49, right associativity).
Definition Not s := Imp s FF.
Lemma satDN I s : I |= Not (Not s) <-> I |= s.
Proof. move: (@satNNPP I s) => /= ; tauto. Qed.
Lemma sat_imp I s t : I |= Imp s t <-> (I |= s -> I |= t).
Proof. done. Qed.
Lemma sat_not I s : I |= Not s <-> ~ I |= s.
Proof. done. Qed.
Definition TT := FF --> FF.
Lemma sat_true I : I |= TT.
Proof. done. Qed.
Definition And s t := Not (Imp s (Not t)).
Notation "s :/\: t" := (And s t) (at level 45).
Lemma sat_and I s t : I |= And s t <-> (I |= s /\ I |= t).
Proof.
rewrite /And /Not /=. split => [A|]; last tauto.
split; apply: satNNPP; tauto.
Qed.
Definition Or s t := Not s --> t.
Notation "s :\/: t" := (Or s t) (at level 47).
Lemma sat_or I s t : I |= s :\/: t <-> I |= s \/ I |= t.
Proof. rewrite /Or /Not /=. split;[case: (satisfies_dec I s)|];tauto. Qed.
Opaque And Or.
Definition Iff s t := (s --> t) :/\: (t --> s).
Notation "s <--> t" := (Iff s t) (at level 50).
Definition All s := Not (Ex (Not s)).
Lemma sat_all I s :
I |= All s <-> (forall N, satisfies (cons N I) s).
Proof.
split => [A N|A].
- apply: satNNPP => B. apply: A. by exists N.
- case: (satisfies_dec I (Ex (Not s))) => //= [[N B]].
exfalso. exact: B.
Qed.
Opaque All.
Emptiness and Singletons
Definition empty X := All (Incl (X.+1) 0).
Lemma sat_empty I X :
I |= empty X <-> I X =i pred0.
Proof.
rewrite sat_all; split => [/= /(_ [::]) A k|A N k]; last by rewrite A.
rewrite inE. apply: negbTE. apply/negP. by move/A.
Qed.
Lemma sat_emptyN I X :
I |= Not (empty X) <-> (exists n, n \in I X).
Proof.
rewrite satDN; split => [[N]|] /=.
- case: (I X) => [|x IX _].
+ by case/(_ _)/Wrap.
+ by exists x; rewrite mem_head.
- case => n A. exists [:: n.+1]. move/(_ _ A). by rewrite inE ltn_eqF.
Qed.
Definition single X := Not(empty X) :/\: All (Not(empty 0) --> Incl 0 X.+1 --> Incl X.+1 0).
Lemma sat_singles I X :
I |= single X <-> exists n, I X =i [:: n].
Proof.
rewrite sat_and sat_emptyN. split.
- move => [[n A] B].
exists n. move => m. rewrite inE. apply/idP/eqP => [H|-> //].
move/sat_all/(_ [:: n]): B. rewrite 2!sat_imp. case/(_ _ _)/Wrap.
+ rewrite sat_emptyN. exists n. by rewrite inE.
+ move => k /=. by rewrite inE => /eqP->.
+ move/(_ _ H). by rewrite inE => /eqP->.
- case => n A. split; first by exists n;rewrite A.
apply/sat_all => N. rewrite 2!sat_imp sat_emptyN => /= [[k Hk] D] m E.
move: (D _ Hk). rewrite A inE => /eqP ?; subst.
rewrite A inE in E. by rewrite (eqP E).
Qed.
Big Operatiors
Notation "\or_ ( i <- r ) F" := (\big [Or/FF]_(i <- r) F)
(at level 42, F at level 42, i at level 0,
format "'[' \or_ ( i <- r ) '/ ' F ']'").
Notation "\or_ ( i \in A ) F" := (\big [Or/FF]_(i <- enum A) F)
(at level 42, F at level 42, i at level 0,
format "'[' \or_ ( i \in A ) '/ ' F ']'").
Notation "\and_ ( i <- r ) F" := (\big [And/TT]_(i <- r) F)
(at level 41, F at level 41, i at level 0,
format "'[' \and_ ( i <- r ) '/ ' F ']'").
Notation "\and_ ( i \in A ) F" := (\big [And/TT]_(i <- enum A) F)
(at level 41, F at level 41, i at level 0,
format "'[' \and_ ( i \in A ) '/ ' F ']'").
Lemma sat_orI (T:eqType) (s : seq T) x F I :
x \in s -> I |= F x -> I |= \or_(i <- s) F i.
Proof. elim: s => // a s IH /predU1P [<-|/IH A]; rewrite big_cons sat_or; tauto. Qed.
Lemma sat_orE (T:eqType) (s : seq T) F I :
I |= \or_(i <- s) F i -> exists2 x, x \in s & I |= F x.
Proof.
elim: s => // [|a s IH]; first by rewrite big_nil.
rewrite big_cons sat_or. case => [A|/IH [x A B]]; first by exists a.
exists x => //. by rewrite inE A orbT.
Qed.
Lemma sat_bigand (T:eqType) (s : seq T) F I :
I |= \and_(i <- s) F i <-> forall x, x \in s -> I |= F x.
Proof.
elim: s => [|a s IH]; first by rewrite big_nil; split => // _; apply.
rewrite big_cons sat_and IH. split => [[A B]x/predU1P[->//|]|A]. exact: B.
split => [|x B]; apply: A => //. by rewrite inE B orbT.
Qed.
First-oder Quantification Note that "first-order" variables are interpreted as one-element lists
rather than directly as numbers. Hence we need the lemmas seq1P and sub1P
Definition All1 s := All (single 0 --> s).
Lemma sat_all1 I s :
I |= All1 s <-> (forall n, cons [:: n] I |= s).
Proof.
rewrite sat_all; split.
- move => H n. move: (H [:: n]) => {H} /=. apply. rewrite sat_singles. by exists n.
- move => H N. rewrite sat_imp sat_singles => [[n Hn]].
apply: weak_coincidence (H n). by case.
Qed.
Definition Ex1 s := Ex (single 0 :/\: s).
Lemma sat_ex1 I s :
I |= Ex1 s <-> (exists n, cons [:: n] I |= s).
Proof.
rewrite /Ex1; split.
- case => N. rewrite -/satisfies => /sat_and [/sat_singles [n] /= B C]. exists n.
apply: weak_coincidence C. by case.
- case => n A. exists [:: n]. apply/sat_and;split => //.
apply/sat_singles. by exists n.
Qed.
Lemma nat_succ x y : y = x.+1 <-> x < y /\ ~ exists k, x < k /\ k < y.
Proof.
split.
- move => ->. rewrite leqnn. split=>//.
move => [k] [A B]. move:(leq_trans A B). by rewrite ltnn.
- move => [A B]. apply/eqP. rewrite eqn_leq leqNgt A andbT.
apply/negP. apply: impliesPn B. constructor.
exists x.+1. by rewrite leqnn H.
Qed.
Definition succ X Y :=
Less X Y :/\: Not (Ex1 (Less X.+1 0 :/\: Less 0 Y.+1)).
Lemma sat_succ I X x Y y : I X =i [:: x] -> I Y =i [:: y] ->
I |= succ X Y <-> y = x.+1.
Proof.
move => A B. rewrite sat_and sat_not sat_ex1 nat_succ.
split => [[C D]|[C D]].
- split; first apply C; rewrite ?A ?B //.
apply: impliesPn D; constructor => [[k [k1 k2]]]. exists k.
rewrite sat_and /=; split => ? ?; by rewrite ?A ?B => /seq1P-> /seq1P->.
- split. move => ? ? ; by rewrite ?A ?B => /seq1P-> /seq1P->.
apply: impliesPn D; constructor => [[k] /sat_and [k1 k2]]. exists k.
split; [apply k1|apply k2]; by rewrite /= ?A ?B.
Qed.
Definition zero X := single X :/\: Not (Ex1 (succ 0 X.+1)).
Lemma sat_zero I X : I X =i [:: 0] <-> I |= zero X.
Proof.
rewrite sat_and sat_singles sat_not sat_ex1.
split.
- move => A. split; first by exists 0.
move => [n]. move/sat_succ. move/(_ 0 n) => /=. by case/(_ _ _)/Wrap.
- move => [[n A] B] k. rewrite A !inE.
suff S : n == 0. apply/idP/idP => /eqP->; by rewrite // eq_sym.
destruct n as [|n] => //. exfalso. apply B.
exists n. by rewrite (sat_succ (x := n) (y := n.+1)).
Qed.
Definition Leq X Y := All1 (succ Y.+1 0 --> Less X.+1 0).
Lemma sat_leq I X x Y y : I X =i [:: x] -> I Y =i [:: y] ->
I |= Leq X Y <-> x <= y.
Proof.
move => A B. rewrite sat_all1. split.
- move/(_ y.+1). rewrite sat_imp. case/(_ _)/Wrap.
+ by rewrite (sat_succ (x := y) (y := y.+1)).
+ move/(_ x y.+1). rewrite /= A !inE ltnS. by apply.
- move => C n. rewrite sat_imp. rewrite (sat_succ (x := y) (y := n)) // => ->.
move => ? ? /=. rewrite A !inE => /eqP-> /eqP->. by rewrite ltnS.
Qed.
Interated existential quantification
Definition cat (Ns: seq (seq nat)) I :=
fun x => if x < size Ns then nth [::] Ns x else I (x - size Ns).
Lemma cat_prefix I n (Ns : n.-tuple (seq nat)) X : X < n -> cat Ns I X = nth [::] Ns X.
Proof. move => A. by rewrite /cat size_tuple A. Qed.
Lemma cat_beyond I n (Ns : n.-tuple (seq nat)) X : n <= X -> cat Ns I X = I (X - n).
Proof. move => A. by rewrite /cat size_tuple ltnNge A. Qed.
Lemma cat_size I n (Ns : n.-tuple (seq nat)) : cat Ns I n = I 0.
Proof. by rewrite cat_beyond ?subnn. Qed.
Definition exn n s := iter n Ex s.
Lemma sat_exn n s I :
(I |= exn n s) <-> (exists Ns : n.-tuple (seq nat), cat Ns I |= s).
Proof.
elim: n I => [|n IH] I.
- split.
+ exists [tuple]. rewrite /cat /=. apply: weak_coincidence H => X. by rewrite subn0.
+ case => Ns. rewrite tuple0 /cat /=.
apply: weak_coincidence => X. by rewrite subn0.
- have agr Ns N X : cat (rcons Ns N) I X =i cat Ns (cons N I) X.
{ rewrite /cat /= !size_rcons ltnS.
case: (ltngtP X (size Ns)) => B.
* by rewrite ?(ltnW B) nth_rcons B.
* try rewrite leqNgt B /=.
by rewrite -[X - size Ns]prednK ?subn_gt0 //= subnS.
* by rewrite ?B ?leqnn ?subnn nth_rcons ltnn eqxx. }
rewrite /=. split => [[N] /IH [Ns A]|].
+ exists [tuple of rcons Ns N]. apply: weak_coincidence A => X k. by rewrite agr.
+ case. case => Ns /=. elim/last_ind : Ns => // Ns N _.
rewrite size_rcons eqSS => A B.
exists N. apply/IH. exists (Tuple A) => /=.
exact: weak_coincidence _ B.
Qed.
Section NFAtoMSO.
Variables (T : finType) (A : nfa T).
Let n := #|A|.
Notation rank := enum_rank.
Notation val := enum_val.
Definition max :=
All1 (Less 0 1 <--> \or_(a \in T) Incl 0 (rank a).+2).
Lemma sat_max (w : word T) m :
cons [:: m] (I_of (vec_of w)) |= max <-> m = size w.
Proof.
split.
- move/sat_all1 => B.
apply/eqP. rewrite eqn_leq [_ <= m]leqNgt [m <= _]leqNgt.
apply/andP; split; apply/negP => C.
+ case: m C B => // m C /(_ m). case/sat_and => [/sat_imp B _]. move: B.
case/(_ _)/Wrap; first by move => ? ? /seq1P-> /seq1P->.
case/sat_orE => a _ /= /sub1P /I_of_vev_max => D. rewrite ltnS in C.
move: (leq_trans D C). by rewrite ltnn.
+ move/(_ m) : B. case/sat_and => _. move/sat_imp.
case/(_ _)/Wrap.
* set a := (tnth (in_tuple w) (Ordinal C)).
apply: (sat_orI (x := a)); first by rewrite mem_enum.
apply/sub1P => /=. by rewrite I_of_vecP // {2}/a (tnth_nth a).
* move/(_ m m) => /=. rewrite !mem_head ltnn. by case/(_ _ _)/Wrap.
- move->.
rewrite sat_all1 => k.
rewrite sat_and; split.
+ rewrite /= => H.
move: H => /(_ k (size w)). case/(_ _ _)/Wrap => // H.
pose a0 := tnth (in_tuple w) (Ordinal H).
apply (sat_orI (x := nth a0 w k)); first by rewrite mem_enum.
rewrite /= => ? /seq1P->. by rewrite I_of_vecP ?(set_nth_default a0).
+ case/sat_orE => a _ /sub1P /=.
rewrite /vec_of /I_of mem_filter => /andP [_].
by rewrite mem_iota add0n size_map /= => H ? ? /seq1P-> /seq1P->.
Qed.
Definition part X :=
All1 (Leq 0 X.+1 -->
(\or_(q \in A) (Incl 0 (rank q).+1 :/\:
\and_(q' \in [pred x | q != x]) Not (Incl 0 (rank q').+1)))).
Lemma sat_part X I k :
I X =i [:: k] ->
I |= part X <-> forall n, n <= k -> exists! q:A, n \in I (rank q).
Proof.
move => H0. split.
- move => H1 m Hm. move/sat_all1 : H1 => /(_ m) /sat_imp. case/(_ _)/Wrap.
+ rewrite sat_leq ; first apply Hm; done.
+ case/sat_orE => q _ /sat_and [/= /sub1P q1 /sat_bigand q2].
exists q; split => // q' B. apply/eqP. apply/negPn/negP => C.
apply: (q2 q'); by [rewrite mem_enum inE|apply/sub1P].
- move => H1.
apply/sat_all1 => m. rewrite sat_imp => /sat_leq H2.
have/H1 {H2} : m <= k by apply: H2.
case => q [q1 q2]. apply: (sat_orI (x := q)); first by rewrite mem_enum.
rewrite sat_and; split; first by move => ? /seq1P ->.
apply/sat_bigand => q'. rewrite mem_enum inE => qq' /sub1P /q2 ?.
subst. by rewrite eqxx in qq'.
Qed.
Definition run X : form :=
All1 (All1(succ 0 1 --> Less 0 X.+2 -->
\or_(paq \in [pred x : A * T * A | nfa_trans x.1.1 x.1.2 x.2])
let: (p,a,q) := paq in
Incl 0 ((rank a).+1 + X).+2
:/\: Incl 0 (rank p).+2
:/\: Incl 1 (rank q).+2
)).
Lemma sat_run (Ns : n.-tuple (seq nat)) m I :
cat Ns (cons [:: m] I) |= run n <->
(forall k, k < m -> exists (p:A) (a:T) (q:A), nfa_trans p a q /\
k \in I (rank a) /\
k \in tnth Ns (rank p) /\
k.+1 \in tnth Ns (rank q)).
Proof.
split.
- move => H k lt_m. move/sat_all1/(_ k.+1) : H. move/sat_all1/(_ k).
rewrite 2!sat_imp. case/(_ _ _)/Wrap.
+ by apply/(sat_succ (x := k) (y := k.+1)).
+ move => /= ? y /seq1P ->. rewrite cat_beyond // subnn /=.
by move/seq1P->.
+ case/sat_orE => [[[p a] q]]. rewrite mem_enum inE /= => B.
rewrite !sat_and. (do 2 case) => /= /sub1P C /sub1P D /sub1P E.
exists p. exists a. exists q. repeat split => //.
* by rewrite cat_beyond ?leq_addl -?addnBA // subnn addn0 in C.
* by rewrite cat_prefix // -tnth_nth in D.
* by rewrite cat_prefix // -tnth_nth in E.
- move => H. apply/sat_all1 => k'. apply/sat_all1 => k. rewrite !sat_imp => B C.
move/sat_succ : B => /(_ k' k). case/(_ _ _)/Wrap => // ?;subst.
case: (H _ (C k m _ _)) => //=; first by rewrite cat_size //=.
move => p [a] [q] [paq [D [E F]]].
apply: (sat_orI (x := (p,a,q))); first by rewrite mem_enum.
rewrite !sat_and; repeat split.
+ apply/sub1P. rewrite /= cat_beyond ?leq_addl //.
rewrite -addnBA // subnn addn0. done.
+ apply/sub1P. by rewrite /= cat_prefix // -tnth_nth.
+ apply/sub1P. by rewrite /= cat_prefix // -tnth_nth.
Qed.
Definition init : form :=
All1 (zero 0 --> \or_(q \in nfa_s A) Incl 0 (rank q).+1).
Lemma sat_init (Ns : n.-tuple (seq nat)) I :
cat Ns I |= init <-> exists2 q, q \in nfa_s A & 0 \in tnth Ns (rank q).
Proof.
split.
- move/sat_all1/(_ 0)/sat_imp. case/(_ _)/Wrap; first exact/sat_zero.
case/sat_orE => s. rewrite mem_enum /= => B /sub1P C. exists s => //.
by rewrite cat_prefix // -tnth_nth in C.
- case => q q1 q2. apply/sat_all1 => m. rewrite sat_imp. move/sat_zero => /= B.
have -> : m = 0. move: (B 0). by rewrite !inE eqxx => /eqP.
apply (sat_orI (x := q)); first by rewrite mem_enum.
apply/sub1P. by rewrite /= cat_prefix -?tnth_nth.
Qed.
Definition accept X := \or_(q \in nfa_fin A) Incl X (rank q).
Lemma sat_accept (Ns : n.-tuple (seq nat)) m I :
cat Ns (cons [:: m] I) |= accept n <->
exists2 q, q \in nfa_fin A & m \in tnth Ns (rank q).
Proof.
split.
- case/sat_orE => q.
rewrite mem_enum /= cat_size ?cat_prefix // -tnth_nth.
move => B /sub1P C. by exists q.
- case => q q1 q2. apply: (sat_orI (x := q)); first by rewrite mem_enum.
rewrite /= cat_size ?cat_prefix // -tnth_nth. exact/sub1P.
Qed.
underneath of exn, #|A| refers to the length of the word (i.e. "max")
Definition form_of :=
Ex1 (max :/\: exn #|A| (
part #|A| :/\: init :/\: run #|A| :/\: accept #|A|)).
Theorem form_ofP w : reflect (@mso_lang T form_of w) (w \in nfa_lang A).
Proof.
apply: (iffP nfaP).
- move =>[s] [r] [r1 r2].
rewrite /mso_lang /vec_lang sat_ex1. exists (size w).
set I' := cons _ _.
have Hmax : I' |= max by apply/sat_max.
rewrite sat_and sat_exn. split => //.
pose pos (i : 'I_#|A|) := [seq n <- iota 0 (size r).+1 | nth s (s::r) n == enum_val i].
pose t := [tuple pos i | i < #|A|].
exists t.
have tP k N (i : 'I_#|A|) :
k \in nth N t i = (k <= size r) && (nth s (s::r) k == val i).
{ by rewrite -tnth_nth tnth_mktuple mem_filter mem_iota /= add0n ltnS andbC. }
rewrite !sat_and; repeat split.
+ apply/(sat_part (k := (size w))). by rewrite cat_size.
move => k Hk. exists (nth s (s::r) k) ;split.
* by rewrite cat_prefix // tP -(run_size r2) Hk enum_rankK eqxx.
* move => q'. rewrite cat_prefix //.
rewrite tP -(run_size r2) Hk enum_rankK. by move/eqP.
+ apply/sat_init. exists s => //. by rewrite tP /= enum_rankK.
+ apply/sat_run => k Hk. have Hk': k < size r by rewrite -(run_size r2).
exists (nth s (s::r) k).
exists (tnth (in_tuple w) (Ordinal Hk)).
exists (nth s (s :: r) k.+1). repeat split.
* exact: run_trans.
* rewrite I_of_vecP //. set X := tnth _ _. by rewrite {2}/X (tnth_nth X).
* by rewrite tP ltnW // enum_rankK eqxx.
* by rewrite tP enum_rankK Hk' eqxx.
+ apply/sat_accept. exists (last s r); first exact: run_last r2.
rewrite tP. by rewrite (run_size r2) leqnn enum_rankK nth_last /=.
- rewrite /mso_lang /vec_lang sat_ex1 => [[m] /sat_and [/sat_max B /sat_exn [Ns]]].
repeat case/sat_and. subst. set I' := cat _ _.
move => /sat_part B /sat_init [s s1 s2] /sat_run D /sat_accept E.
move: {B} (B (size w)).
case/(_ _)/Wrap => [k|B]; first by rewrite /I' cat_size.
have exP (i : 'I_(size w)) : exists q : A, i.+1 \in I' (rank q).
{ case: (B i.+1)=> // q [q1 q2]. by exists q. }
exists s. pose r := [tuple xchoose (exP i) | i < size w]. exists r. split => //.
have tP k p : k <= size w -> k \in tnth Ns (rank p) -> nth s (s::r) k = p.
{ case: k => [_|k lt_w] H /=.
- case: (B 0 _) => // q' [q1 q2].
by rewrite -[p]q2 -1?[s]q2 // /I' cat_prefix // -tnth_nth.
- rewrite (nth_map (Ordinal lt_w)) ?size_enum_ord //.
set m := nth _ _ _. move: (exP _) => F. move: (xchooseP F) => G.
case: (B m.+1 _) => // q' [q1 q2].
rewrite -[xchoose F]q2 -1?[p]q2 //.
rewrite /I' cat_prefix // -tnth_nth.
by rewrite /m nth_enum_ord.
}
apply: runI.
+ by rewrite size_tuple.
+ case: E => f f1 f2. rewrite (_ : last s r = f) //.
by rewrite (last_nth s) size_tuple (tP _ _ _ f2).
+ move => i. move: (D _ (ltn_ord i)) => [p] [a] [q] [pq [Ha [Hp Hq]]].
rewrite I_of_vecP // in Ha. rewrite (tnth_nth a) (eqP Ha) //.
by rewrite (tP _ _ _ Hp) 1?ltnW // (tP _ _ _ Hq).
Qed.
End NFAtoMSO.
Ex1 (max :/\: exn #|A| (
part #|A| :/\: init :/\: run #|A| :/\: accept #|A|)).
Theorem form_ofP w : reflect (@mso_lang T form_of w) (w \in nfa_lang A).
Proof.
apply: (iffP nfaP).
- move =>[s] [r] [r1 r2].
rewrite /mso_lang /vec_lang sat_ex1. exists (size w).
set I' := cons _ _.
have Hmax : I' |= max by apply/sat_max.
rewrite sat_and sat_exn. split => //.
pose pos (i : 'I_#|A|) := [seq n <- iota 0 (size r).+1 | nth s (s::r) n == enum_val i].
pose t := [tuple pos i | i < #|A|].
exists t.
have tP k N (i : 'I_#|A|) :
k \in nth N t i = (k <= size r) && (nth s (s::r) k == val i).
{ by rewrite -tnth_nth tnth_mktuple mem_filter mem_iota /= add0n ltnS andbC. }
rewrite !sat_and; repeat split.
+ apply/(sat_part (k := (size w))). by rewrite cat_size.
move => k Hk. exists (nth s (s::r) k) ;split.
* by rewrite cat_prefix // tP -(run_size r2) Hk enum_rankK eqxx.
* move => q'. rewrite cat_prefix //.
rewrite tP -(run_size r2) Hk enum_rankK. by move/eqP.
+ apply/sat_init. exists s => //. by rewrite tP /= enum_rankK.
+ apply/sat_run => k Hk. have Hk': k < size r by rewrite -(run_size r2).
exists (nth s (s::r) k).
exists (tnth (in_tuple w) (Ordinal Hk)).
exists (nth s (s :: r) k.+1). repeat split.
* exact: run_trans.
* rewrite I_of_vecP //. set X := tnth _ _. by rewrite {2}/X (tnth_nth X).
* by rewrite tP ltnW // enum_rankK eqxx.
* by rewrite tP enum_rankK Hk' eqxx.
+ apply/sat_accept. exists (last s r); first exact: run_last r2.
rewrite tP. by rewrite (run_size r2) leqnn enum_rankK nth_last /=.
- rewrite /mso_lang /vec_lang sat_ex1 => [[m] /sat_and [/sat_max B /sat_exn [Ns]]].
repeat case/sat_and. subst. set I' := cat _ _.
move => /sat_part B /sat_init [s s1 s2] /sat_run D /sat_accept E.
move: {B} (B (size w)).
case/(_ _)/Wrap => [k|B]; first by rewrite /I' cat_size.
have exP (i : 'I_(size w)) : exists q : A, i.+1 \in I' (rank q).
{ case: (B i.+1)=> // q [q1 q2]. by exists q. }
exists s. pose r := [tuple xchoose (exP i) | i < size w]. exists r. split => //.
have tP k p : k <= size w -> k \in tnth Ns (rank p) -> nth s (s::r) k = p.
{ case: k => [_|k lt_w] H /=.
- case: (B 0 _) => // q' [q1 q2].
by rewrite -[p]q2 -1?[s]q2 // /I' cat_prefix // -tnth_nth.
- rewrite (nth_map (Ordinal lt_w)) ?size_enum_ord //.
set m := nth _ _ _. move: (exP _) => F. move: (xchooseP F) => G.
case: (B m.+1 _) => // q' [q1 q2].
rewrite -[xchoose F]q2 -1?[p]q2 //.
rewrite /I' cat_prefix // -tnth_nth.
by rewrite /m nth_enum_ord.
}
apply: runI.
+ by rewrite size_tuple.
+ case: E => f f1 f2. rewrite (_ : last s r = f) //.
by rewrite (last_nth s) size_tuple (tP _ _ _ f2).
+ move => i. move: (D _ (ltn_ord i)) => [p] [a] [q] [pq [Ha [Hp Hq]]].
rewrite I_of_vecP // in Ha. rewrite (tnth_nth a) (eqP Ha) //.
by rewrite (tP _ _ _ Hp) 1?ltnW // (tP _ _ _ Hq).
Qed.
End NFAtoMSO.