proposition: Lemma empty_is_empty : forall T (s : list T), ~ (s =~ EmptySet).
proof: Proof. Admitted. Lemma MUnion' : forall T (s : list T) (re1 re2 : reg_exp T), s =~ re1 \/ s =~ re2 -> s =~ Union re1 re2. Proof. Admitted. Lemma MStar' : forall T (ss : list (list T)) (re : reg_exp T), (forall s, In s ss -> s =~ re) -> fold app ss [] =~ Star re. Proof. Admitted. Fixpoint re_chars {T} (re : reg_exp T) : list T := match re with | EmptySet => [] | EmptyStr => [] | Char x => [x] | App re1 re2 => re_chars re1 ++ re_chars re2 | Union re1 re2 => re_chars re1 ++ re_chars re2 | Star re => re_chars re end. Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T), s =~ re -> In x s -> In x (re_chars re). Proof. intros T s re x Hmatch Hin. 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 in Hin. destruct Hin. - simpl. simpl in Hin. apply Hin. - simpl. rewrite In_app_iff in *. destruct Hin as [Hin | Hin]. + left. apply (IH1 Hin). + right. apply (IH2 Hin). - simpl. rewrite In_app_iff. left. apply (IH Hin). - simpl. rewrite In_app_iff. right. apply (IH Hin). - destruct Hin. - simpl. rewrite In_app_iff in Hin. destruct Hin as [Hin | Hin]. + apply (IH1 Hin). + apply (IH2 Hin). Qed.
imports: Coq(Lia)