Section Logic1. Variable A : Type. Variables P Q : A -> Prop. Variable R : A -> A-> Prop. Lemma L1 : (forall x y , R x y -> Q y) <-> (forall y, (exists x, R x y) -> Q y). Proof. split. - intros H y H0;destruct H0 as [x Hx]. now apply (H x). - intros H x y H0. apply H; exists x;auto. Qed. Lemma L2 : (forall x, ~ (P x /\ Q x)) -> (exists x, P x) -> (exists y, ~ Q y). Proof. intros H H0; destruct H0 as [x Hx]. exists x; intro H1; destruct (H x). split; assumption. Qed. Section S1. Hypothesis R_trans : forall x y z, R x y -> R y z -> R x z. Hypothesis R_sym : forall x y, R x y -> R y x. Hypothesis R_irrefl : forall x, ~ R x x. Lemma R_is_empty : ~ (exists x y:A, R x y). Proof. intro H; destruct H as [x Hx]. destruct Hx as [y Hxy]. destruct (R_irrefl x). apply (R_trans x y x);auto. Qed. End S1. End Logic1. Section Logic2. Definition my_or (P Q : Prop) : Prop := forall A:Prop, (P -> A) -> (Q -> A) -> A. (** give this proof as an example *) Lemma my_or_intro_l : forall P Q: Prop, P -> my_or P Q. Proof. intros P Q H A H0 H1;apply H0;assumption. Qed. Lemma my_or_intro_r : forall P Q: Prop, Q -> my_or P Q. Proof. intros P Q H A H0 H1;apply H1;assumption. Qed. Lemma my_or_elim : forall P Q R: Prop, (P -> R) -> (Q -> R) -> my_or P Q -> R. Proof. unfold my_or; intros. apply H1;assumption. Qed. Lemma my_or_False : forall P:Prop, my_or P False -> P. Proof. intros P H; apply H. intro; assumption. contradiction. Qed. Lemma my_or_iff : forall P Q:Prop, my_or P Q <-> P \/ Q. Proof. split. - intro H; apply H. left;assumption. right;assumption. - intro H; destruct H. + now apply my_or_intro_l. + now apply my_or_intro_r. Qed. End Logic2. (*** On Bintrees *) Inductive bintree (A : Type) := | leaf | bin (root:A)(l_son r_son : bintree A ). Fixpoint In_tree {A}(a:A) (t : bintree A) := match t with | leaf => False | bin r t1 t2 => a = r \/ In_tree a t1 \/ In_tree a t2 end. Require Import List. Fixpoint inorder_traversal {A}(t: bintree A) : list A := match t with | leaf => nil | bin r t1 t2 => inorder_traversal t1 ++ (r :: inorder_traversal t2) end. Fixpoint Member {A}(a:A)(l: list A) := match l with nil => False | x::l' => a=x \/ Member a l' end. Lemma Member_app_1 {A}: forall (a:A) l1 l2, Member a l1 -> Member a (l1 ++ l2). Proof. induction l1;simpl. intros;contradiction. intros l2 H; destruct H. - now left. - right;apply IHl1;auto. Qed. Lemma Member_app_2 {A}: forall (a:A) l1 l2, Member a l2 -> Member a (l1 ++ l2). Proof. - induction l1;simpl. + intros;assumption. + right; now apply IHl1. Qed. Lemma Member_app_cases {A}: forall (a:A) l1 l2, Member a (l1 ++ l2) -> Member a l1 \/ Member a l2. Proof. induction l1;simpl;auto. - intros l2 H; destruct H. repeat left;assumption. destruct (IHl1 l2 H). left;right;assumption. now right. Qed. Lemma Member_app_iff {A}: forall (a:A) l1 l2, Member a (l1 ++ l2) <-> Member a l1 \/ Member a l2. Proof. intros a l1 l2;split. - intro H; destruct (Member_app_cases _ _ _ H). + now left. + now right. - intro H; destruct H. + now apply Member_app_1. + now apply Member_app_2. Qed. Lemma in_tree_Member {A} : forall a (t:bintree A), In_tree a t -> Member a (inorder_traversal t). Proof. induction t. - simpl. intro;assumption. - simpl. intro H; destruct H. rewrite H; apply Member_app_2. simpl; now left. destruct H. apply Member_app_1;now apply IHt1. apply Member_app_2. simpl;right; now apply IHt2. Qed.