proposition: Lemma re_opt_match'' : forall T (re: reg_exp T) s, s =~ re -> s =~ re_opt re.
proof: Proof. Admitted. Definition manual_grade_for_re_opt_match'' : option (nat*string) := None. Import Pumping. 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. Admitted. Definition manual_grade_for_pumping_redux : option (nat*string) := None. 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. Admitted. Definition manual_grade_for_pumping_redux_strong : option (nat*string) := None. Example trans_example1: forall a b c d, a <= b + b * c -> (1 + c) * b <= d -> a <= d. Proof. intros a b c d H1 H2. apply le_trans with (b + b * c). - apply H1. - simpl in H2. rewrite mul_comm. apply H2. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)