proposition: Lemma MStar1 : forall T s (re : reg_exp T) , s =~ re -> s =~ Star re.
proof: Proof. Admitted. Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T), s1 =~ Star re -> s2 =~ Star re -> s1 ++ s2 =~ Star re. Proof. intros T s1 s2 re H1. generalize dependent s2. induction H1 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 s2 H. apply H. - intros s2 H. simpl. Abort. Lemma star_app: forall T (s1 s2 : list T) (re re' : reg_exp T), re' = Star re -> s1 =~ re' -> s2 =~ Star re -> s1 ++ s2 =~ Star re. Abort. Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T), s1 =~ Star re -> s2 =~ Star re -> s1 ++ s2 =~ Star re. Proof. intros T s1 s2 re H1. remember (Star re) as re'. generalize dependent s2. induction H1 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]. - discriminate. - discriminate. - discriminate. - discriminate. - discriminate. - injection Heqre' as Heqre''. intros s H. apply H. - injection Heqre' as Heqre''. intros s2 H1. rewrite <- app_assoc. apply MStarApp. + apply Hmatch1. + apply IH2. * rewrite Heqre''. reflexivity. * apply H1. Qed.
imports: Coq(Lia)