proposition: Lemma pump_dfa (A : dfa char) x y z : x ++ y ++ z \in dfa_lang A -> #|A| < size y -> exists u v w, [/\ ~~ nilp v, y = u ++ v ++ w & forall i, (x ++ u ++ rep v i ++ w ++ z) \in dfa_lang A].
proof: Proof. rewrite -delta_lang => H1 H2. have/injectivePn : ~~ injectiveb (fun i : 'I_(size y) => delta (delta_s A x) (take i y)). apply: contraL H2 => /injectiveP/leq_card. by rewrite leqNgt card_ord. move => [i] [j] ij fij. wlog {ij} ij : i j fij / i < j. rewrite neq_ltn in ij. case/orP : ij => ij W; exact: W _ ij. exists (take i y), (sub i j y), (drop j y). split => [||k]. - apply: contraL ij. by rewrite /nilp size_take size_drop ltn_sub2r ?ltn_ord // subn_eq0 leqNgt. - by rewrite catA -takeD subnKC 1?ltnW // cat_take_drop. - rewrite inE /dfa_accept !delta_cat delta_rep. by rewrite fij -!delta_cat !catA -[(x ++ _) ++ _]catA cat_take_drop -!catA. rewrite -delta_cat -takeD subnKC //. exact: ltnW. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)