proposition: 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: 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_sup_seq i_in_X _ _. by rewrite /i addSn -ltn_subRL subnn. + move/hasPn => /= B. 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.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)