proposition: Lemma weak_pumping : forall T (re : reg_exp T) s, s =~ re -> pumping_constant re <= length s -> exists s1 s2 s3, s = s1 ++ s2 ++ s3 /\ s2 <> [] /\ forall m, s1 ++ napp m s2 ++ s3 =~ re.
proof: Proof. intros T re s Hmatch. induction Hmatch as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ]. - simpl. intros contra. inversion contra. Admitted. Lemma pumping : forall T (re : reg_exp T) s, s =~ re -> pumping_constant re <= length s -> exists s1 s2 s3, s = s1 ++ s2 ++ s3 /\ s2 <> [] /\ length s1 + length s2 <= pumping_constant re /\ forall m, s1 ++ napp m s2 ++ s3 =~ re. Proof. intros T re s Hmatch. induction Hmatch as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ]. - simpl. intros contra. inversion contra. Admitted. End Pumping. Theorem filter_not_empty_In : forall n l, filter (fun x => n =? x) l <> [] -> In n l. Proof. intros n l. induction l as [|m l' IHl']. - simpl. intros H. apply H. reflexivity. - simpl. destruct (n =? m) eqn:H. + intros _. rewrite eqb_eq in H. rewrite H. left. reflexivity. + intros H'. right. apply IHl'. apply H'. Qed.
imports: Coq(Lia)