proposition: Theorem form_ofP w : reflect (@mso_lang T form_of w) (w \in nfa_lang A).
proof: 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), (tnth (in_tuple w) (Ordinal Hk)), (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.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)