proposition: Theorem ev100: ev 100.
proof: Proof. Admitted. Fixpoint re_opt {T:Type} (re: reg_exp T) : reg_exp T := match re with | App _ EmptySet => EmptySet | App EmptyStr re2 => re_opt re2 | App re1 EmptyStr => re_opt re1 | App re1 re2 => App (re_opt re1) (re_opt re2) | Union EmptySet re2 => re_opt re2 | Union re1 EmptySet => re_opt re1 | Union re1 re2 => Union (re_opt re1) (re_opt re2) | Star EmptySet => EmptyStr | Star EmptyStr => EmptyStr | Star re => Star (re_opt re) | EmptySet => EmptySet | EmptyStr => EmptyStr | Char x => Char x end. Lemma re_opt_match : forall T (re: reg_exp T) s, s =~ re -> s =~ re_opt re. Proof. intros T re s M. induction M 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. apply MEmpty. - simpl. apply MChar. - simpl. destruct re1. + inversion IH1. + inversion IH1. simpl. destruct re2. * apply IH2. * apply IH2. * apply IH2. * apply IH2. * apply IH2. * apply IH2. + destruct re2. * inversion IH2. * inversion IH2. rewrite app_nil_r. apply IH1. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. + destruct re2. * inversion IH2. * inversion IH2. rewrite app_nil_r. apply IH1. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. + destruct re2. * inversion IH2. * inversion IH2. rewrite app_nil_r. apply IH1. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. + destruct re2. * inversion IH2. * inversion IH2. rewrite app_nil_r. apply IH1. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. * apply MApp. -- apply IH1. -- apply IH2. - simpl. destruct re1. + inversion IH. + destruct re2. * apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. + destruct re2. * apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. + destruct re2. * apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. + destruct re2. * apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. + destruct re2. * apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. * apply MUnionL. apply IH. - simpl. destruct re1. + apply IH. + destruct re2. * inversion IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. + destruct re2. * inversion IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. + destruct re2. * inversion IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. + destruct re2. * inversion IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. + destruct re2. * inversion IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. * apply MUnionR. apply IH. - simpl. destruct re. + apply MEmpty. + apply MEmpty. + apply MStar0. + apply MStar0. + apply MStar0. + simpl. destruct re. * apply MStar0. * apply MStar0. * apply MStar0. * apply MStar0. * apply MStar0. * apply MStar0. - simpl. destruct re. + inversion IH1. + inversion IH1. inversion IH2. apply MEmpty. + apply star_app. * apply MStar1. apply IH1. * apply IH2. + apply star_app. * apply MStar1. apply IH1. * apply IH2. + apply star_app. * apply MStar1. apply IH1. * apply IH2. + apply star_app. * apply MStar1. apply IH1. * apply IH2. Qed.
imports: Coq(Arith List) LF(IndProp)