proposition: Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
proof: Proof. Admitted. Theorem O_le_n : forall n, 0 <= n. Proof. Admitted. Theorem n_le_m__Sn_le_Sm : forall n m, n <= m -> S n <= S m. Proof. Admitted. Theorem Sn_le_Sm__n_le_m : forall n m, S n <= S m -> n <= m. Proof. Admitted. Theorem le_plus_l : forall a b, a <= a + b. Proof. Admitted. Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m. Proof. unfold lt. Admitted. Theorem lt_S : forall n m, n < m -> n < S m. Proof. Admitted. Theorem leb_complete : forall n m, leb n m = true -> n <= m. Proof. Admitted. Theorem leb_correct : forall n m, n <= m -> leb n m = true. Proof. Admitted. Theorem leb_true_trans : forall n m o, leb n m = true -> leb m o = true -> leb n o = true. Proof. Admitted. Theorem leb_iff : forall n m, leb n m = true <-> n <= m. Proof. Admitted. Module R. Inductive R : nat -> nat -> nat -> Prop := | c1 : R 0 0 0 | c2 : forall m n o, R m n o -> R (S m) n (S o) | c3 : forall m n o, R m n o -> R m (S n) (S o) | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o | c5 : forall m n o, R m n o -> R n m o. Definition fR : nat -> nat -> nat . Admitted. Theorem R_equiv_fR : forall m n o, R m n o <-> fR m n = o. Proof. Admitted. End R. Inductive reg_exp (T : Type) : Type := | EmptySet : reg_exp T | EmptyStr : reg_exp T | Char : T -> reg_exp T | App : reg_exp T -> reg_exp T -> reg_exp T | Union : reg_exp T -> reg_exp T -> reg_exp T | Star : reg_exp T -> reg_exp T. Arguments EmptySet {T}. Arguments EmptyStr {T}. Arguments Char {T} _. Arguments App {T} _ _. Arguments Union {T} _ _. Arguments Star {T} _. Inductive exp_match {T} : list T -> reg_exp T -> Prop := | MEmpty : exp_match [] EmptyStr | MChar : forall x, exp_match [x] (Char x) | MApp : forall s1 re1 s2 re2, exp_match s1 re1 -> exp_match s2 re2 -> exp_match (s1 ++ s2) (App re1 re2) | MUnionL : forall s1 re1 re2, exp_match s1 re1 -> exp_match s1 (Union re1 re2) | MUnionR : forall re1 s2 re2, exp_match s2 re2 -> exp_match s2 (Union re1 re2) | MStar0 : forall re, exp_match [] (Star re) | MStarApp : forall s1 s2 re, exp_match s1 re -> exp_match s2 (Star re) -> exp_match (s1 ++ s2) (Star re). Notation "s =~ re" := (exp_match s re) (at level 80). Example reg_exp_ex1 : [1] =~ Char 1. Proof. apply MChar. Qed.
imports: Logic