Module Predicate. (* Some useful tactics *) Require ClassicalFacts. (* no axioms in this line *) Require Export Coq.Logic.ClassicalChoice. Tactic Notation "LEM" constr(a) := destruct (classic a). Tactic Notation "spec" hyp(H) := match type of H with ?a -> _ => let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end. Tactic Notation "spec" hyp(H) constr(a) := (generalize (H a); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) := (generalize (H a b); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) := (generalize (H a b c); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) := (generalize (H a b c d); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) := (generalize (H a b c d e); clear H; intro H). Parameter term : Type. Lemma ExistsForall: forall (P : term -> term -> Prop), (exists y, forall x, P x y) -> (forall x, exists y, P x y). Proof. intros. destruct H. exists x0. spec H x. apply H. Qed. Lemma ForallConj: forall (P Q : term -> Prop), ((forall x, P x) /\ (forall x, Q x)) -> forall x, P x /\ Q x. Proof. intros. destruct H. split. apply H. apply H0. Qed. Lemma ForallConj2: forall (P Q : term -> Prop), (forall x, P x /\ Q x) -> ((forall x, P x) /\ (forall x, Q x)). Proof. admit. Qed. Lemma ExistsDisj: forall (P Q : term -> Prop), ((exists x, P x) \/ (exists x, Q x)) -> exists x, P x \/ Q x. Proof. intros. destruct H. destruct H. exists x. left. apply H. destruct H. exists x. right. apply H. Qed. Lemma ExistsDisj2 : forall (P Q : term -> Prop), ((exists x, P x) \/ (exists x, Q x)) -> (exists x, P x \/ Q x). Proof. admit. Qed. Lemma NotForallQX: forall P Q : term -> Prop, (exists x, P x) -> (forall x, Q x -> ~P x) -> ~forall x, Q x. Proof. admit. Qed. Lemma deMorgan: forall (P : term -> Prop), (forall x, P x) -> ~ (exists x, ~P x). Proof. intros. unfold not. intro. destruct H0. apply H0. spec H x. apply H. Qed. Lemma deMorgan2 : forall (P : term -> Prop), (exists x, P x) -> (~forall x, ~P x). Proof. intros. unfold not. intro. destruct H. spec H0 x. apply H0. apply H. Qed. Lemma deMorgan3 : forall (P : term -> Prop), (~forall x, ~P x) -> (exists x, P x). Proof. intros. LEM (exists x, P x). apply H0. unfold not in H. exfalso. apply H. intro. intro. unfold not in H0. apply H0. exists x. apply H1. Qed. Lemma Irreflexive1: forall (P Q : term -> term -> Prop), (forall x y, P x y -> P y x -> Q x y) -> (forall x, ~ Q x x) -> ~(exists x, P x x). Proof. intros. intro. destruct H1. spec H x x. spec H0 x. unfold not in H0. apply H0. apply H. apply H1. apply H1. Qed. Lemma Irreflexive2: forall P : term -> term -> Prop, (forall x y, P x y -> P y x -> ~ x = y) -> ~exists x, P x x. Proof. intros. intro. destruct H0. spec H x x. apply H in H0. apply H0. trivial. apply H0. Qed. Lemma ReflexiveOnly1: forall P : term -> term -> Prop, (forall x y, P x y -> P y x) -> (forall x y z, P x y -> P y z -> P x z) -> forall x y, P x y -> P x x. Proof. intros. spec H x y. spec H0 x y x. apply H0. apply H1. apply H. apply H1. Qed. Lemma ReflexiveOnly2: forall P : term -> term -> Prop, (forall x, ~exists y, (P x y) /\ (~P y x)) -> (forall x y z, P x y -> P y z -> P x z) -> (forall x y, P x y -> P x x). Proof. intros. spec H0 x y x. LEM (P x x). apply H2. apply H0. apply H1. spec H x. unfold not in H. exfalso. apply H. exists y. split. apply H1. intro. unfold not in H2. apply H2. apply H0. apply H1. apply H3. Qed. Lemma XXX: forall (P Q : term -> term -> term -> Prop), (forall x y, (exists z, Q x y z) -> forall z, Q x y z -> P x x z) -> (exists a, Q a a a) -> exists x, P x x x. Proof. intros. destruct H0. exists x. spec H x x. apply H. exists x. apply H0. apply H0. Qed. Lemma XequalsY: forall (P : term -> term -> Prop) (f : term -> term), (forall x y, f x = f y -> P x y -> x = y) -> (forall x y, P (f x) (f y) -> P x y) -> (forall x y, P x y -> P y x -> x = y) -> (forall x y, P (f x) (f y) -> P (f y) (f x)) -> (forall x y, P (f x) (f y) -> x = y). Proof. intros. spec H2 x y. spec H2 H3. assert (P x y). apply H0. apply H3. spec H0 y x. spec H0 H2. apply H1. apply H4. apply H0. Qed.