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 lt_ge_cases : forall n m, n < m \/ n >= m. Proof. Admitted. Theorem le_plus_l : forall a b, a <= a + b. Proof. Admitted. Theorem plus_le : forall n1 n2 m, n1 + n2 <= m -> n1 <= m /\ n2 <= m. Proof. Admitted. Theorem add_le_cases : forall n m p q, n + m <= p + q -> n <= p \/ m <= q. Proof. Admitted. Theorem plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. Proof. Admitted. Theorem plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p. Proof. Admitted. Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p. Proof. Admitted. Theorem n_lt_m__n_le_m : forall n m, n < m -> n <= m. Proof. Admitted. Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m. Proof. Admitted. Theorem leb_complete : forall n m, n <=? m = true -> n <= m. Proof. Admitted. Theorem leb_correct : forall n m, n <= m -> n <=? m = true. Proof. Admitted. Theorem leb_true_trans : forall n m o, n <=? m = true -> m <=? o = true -> n <=? o = true. Proof. Admitted. Theorem leb_iff : forall n m, n <=? m = true <-> n <= m. Proof. Admitted. Module R. Inductive R : nat -> nat -> nat -> Prop := | c1 : R 0 0 0 | c2 m n o (H : R m n o ) : R (S m) n (S o) | c3 m n o (H : R m n o ) : R m (S n) (S o) | c4 m n o (H : R (S m) (S n) (S (S o))) : R m n o | c5 m n o (H : R m n o ) : R n m o . Definition manual_grade_for_R_provability : option (nat*string) := None. 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 subseq : list nat -> list nat -> Prop := . Theorem subseq_refl : forall (l : list nat), subseq l l. Proof. Admitted. Theorem subseq_app : forall (l1 l2 l3 : list nat), subseq l1 l2 -> subseq l1 (l2 ++ l3). Proof. Admitted. Theorem subseq_trans : forall (l1 l2 l3 : list nat), subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3. Proof. Admitted. Module bin1. Inductive bin : Type := | Z | B0 (n : bin) | B1 (n : bin). End bin1. Module bin2. Inductive bin : Type := | Z : bin | B0 (n : bin) : bin | B1 (n : bin) : bin. End bin2. Module bin3. Inductive bin : Type := | Z : bin | B0 : bin -> bin | B1 : bin -> bin. End bin3. Inductive reg_exp (T : Type) : Type := | EmptySet | EmptyStr | Char (t : T) | App (r1 r2 : reg_exp T) | Union (r1 r2 : reg_exp T) | Star (r : reg_exp T). Arguments EmptySet {T}. Arguments EmptyStr {T}. Arguments Char {T} _. Arguments App {T} _ _. Arguments Union {T} _ _. Arguments Star {T} _. Reserved Notation "s =~ re" (at level 80). Inductive exp_match {T} : list T -> reg_exp T -> Prop := | MEmpty : [] =~ EmptyStr | MChar x : [x] =~ (Char x) | MApp s1 re1 s2 re2 (H1 : s1 =~ re1) (H2 : s2 =~ re2) : (s1 ++ s2) =~ (App re1 re2) | MUnionL s1 re1 re2 (H1 : s1 =~ re1) : s1 =~ (Union re1 re2) | MUnionR re1 s2 re2 (H2 : s2 =~ re2) : s2 =~ (Union re1 re2) | MStar0 re : [] =~ (Star re) | MStarApp s1 s2 re (H1 : s1 =~ re) (H2 : s2 =~ (Star re)) : (s1 ++ s2) =~ (Star re) where "s =~ re" := (exp_match s re). Example reg_exp_ex1 : [1] =~ Char 1. Proof. apply MChar. Qed.
imports: Coq(Lia)