proposition: Theorem test_le1 : 3 <= 3.
proof: Proof. Admitted. Theorem test_le2 : 3 <= 6. Proof. Admitted. Theorem test_le3 : (2 <= 1) -> 2 + 2 = 5. Proof. Admitted. Definition lt (n m : nat) := le (S n) m. Notation "m < n" := (lt m n). End Playground. 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)