Require Import NaturalDeduction. Lemma L15a (P : Prop) : P <-> ~~P. Proof. unfold iff; And_Intro. Impl_Intro. Not_Intro. Not_Elim in H0 and H. assumption. Impl_Intro. PBC. Not_Elim in H and H0. assumption. Qed. Lemma L15d (P : Prop) : P \/ ~P. Proof. PBC. assume (P \/ ~P). Not_Elim in H and H0. assumption. Or_Intro_2. Not_Intro. assume (P \/ ~P). Not_Elim in H and H1. assumption. Or_Intro_1. assumption. Qed. Lemma L15e (P Q : Prop) : (P -> Q) <-> ~P \/ Q. Proof. unfold iff; And_Intro. Impl_Intro. PBC. assume (~P \/ Q). Not_Elim in H0 and H1. assumption. Or_Intro_2. assume P. Impl_Elim in H and H1. assumption. PBC. assume (~P \/ Q). Not_Elim in H0 and H2. assumption. Or_Intro_1. assumption. Impl_Intro. Impl_Intro. Or_Elim in H. Not_Elim in H and H0. PBC. assumption. assumption. Qed. Lemma L15f (P Q : Prop) : ~(P -> Q) <-> P /\ ~Q. Proof. unfold iff; And_Intro. Impl_Intro. And_Intro. PBC. assume (P -> Q). Not_Elim in H and H1. assumption. Impl_Intro. Not_Elim in H0 and H1. PBC. assumption. Not_Intro. assume (P -> Q). Not_Elim in H and H1. assumption. Impl_Intro. assumption. Impl_Intro. Not_Intro. And_Elim_1 in H. Impl_Elim in H0 and H1. And_Elim_2 in H. Not_Elim in H2 and H3. assumption. Qed. Lemma Example (P Q : Prop) : (~P -> Q) -> (~Q -> P). Proof. Impl_Intro. Impl_Intro. PBC. Impl_Elim in H and H1. Not_Elim in H0 and H3. assumption. Qed. Lemma Example_generated (P Q : Prop) : (~P -> Q) -> (~Q -> P). Proof. (* Case distinction P,~P *) assert(H:=L15d P). Or_Elim in H. (* Case distinction Q,~Q *) assert(H1:=L15d Q). Or_Elim in H1. (* Case P,Q as assumptions*) assume(~(~P -> Q) \/ (~Q -> P)). assert(H2:=L15e (~P -> Q) (~Q -> P)) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_2. assume(~~Q \/ P). assert(H2:=L15e (~Q) P) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_2. assumption. (* Case P,~Q as assumptions*) assume(~(~P -> Q) \/ (~Q -> P)). assert(H2:=L15e (~P -> Q) (~Q -> P)) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_2. assume(~~Q \/ P). assert(H2:=L15e (~Q) P) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_2. assumption. (* Case distinction Q,~Q *) assert(H1:=L15d Q). Or_Elim in H1. (* Case ~P,Q as assumptions*) assume(~(~P -> Q) \/ (~Q -> P)). assert(H2:=L15e (~P -> Q) (~Q -> P)) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_2. assume(~~Q \/ P). assert(H2:=L15e (~Q) P) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_1. assert(H1:=L15a Q). unfold iff in H1; And_Elim_1 in H1. Impl_Elim in H2 and H0. assumption. (* Case ~P,~Q as assumptions*) assume(~(~P -> Q) \/ (~Q -> P)). assert(H2:=L15e (~P -> Q) (~Q -> P)) . unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. Or_Intro_1. assume(~P /\ ~Q). assert(H2:=L15f (~P) Q). unfold iff in H2; And_Elim_2 in H2. Impl_Elim in H3 and H1. assumption. And_Intro. assumption. assumption. Qed. Lemma L43a (A : Type) (P : A -> Prop) : (forall x, P x) <-> (forall y, P y). Proof. unfold iff; And_Intro. Impl_Intro. Forall_Intro. Forall_Elim in H with y. assumption. Impl_Intro. Forall_Intro. Forall_Elim in H with x. assumption. Qed. Lemma L43a' (A : Type) (P : A -> Prop) : (forall x, P x) <-> (forall y, P y). Proof. assert ((forall x : A, P x) -> (forall y : A, P y)). Impl_Intro. Forall_Intro. Forall_Elim in H with y. assumption. unfold iff; And_Intro; apply H. Qed. Lemma L43b (A : Type) (P : A -> Prop) : (exists x, P x) <-> (exists y, P y). Proof. assert ((exists x, P x) -> (exists y, P y)). Impl_Intro. Exists_Elim in H. Exists_Intro with x. assumption. unfold iff; And_Intro; apply H. Qed. Lemma L65a (A : Type) (P : A -> A -> Prop) : (forall x y, P x y) <-> (forall y x, P x y). Proof. unfold iff; And_Intro. Impl_Intro. Forall_Intro. Forall_Intro. Forall_Elim in H with x. Forall_Elim in H1 with y. assumption. Impl_Intro. Forall_Intro. Forall_Intro. Forall_Elim in H with y. Forall_Elim in H1 with x. assumption. Qed. Lemma L65b (A : Type) (P : A -> A -> Prop) : (exists x y, P x y) <-> (exists y x, P x y). Proof. unfold iff; And_Intro. Impl_Intro. Exists_Elim in H. Exists_Elim in H0. Exists_Intro with x0. Exists_Intro with x. assumption. Impl_Intro. Exists_Elim in H. Exists_Elim in H0. Exists_Intro with x0. Exists_Intro with x. assumption. Qed. Lemma L65c (A : Type) (P : A -> Prop) : ~(forall x, P x) <-> (exists x, ~P x). Proof. unfold iff; And_Intro. Impl_Intro. PBC. assume (forall x : A, P x). Not_Elim in H and H1. assumption. Forall_Intro. PBC. assume (exists x : A, ~ P x). Not_Elim in H0 and H2. assumption. Exists_Intro with x. assumption. Impl_Intro. Not_Intro. Exists_Elim in H. Forall_Elim in H0 with x. Not_Elim in H1 and H3. assumption. Qed. Lemma L65d (A : Type) (P : A -> Prop) : ~(exists x, P x) <-> (forall x, ~P x). Proof. unfold iff; And_Intro. Impl_Intro. Forall_Intro. Not_Intro. assume (exists x : A, P x). Not_Elim in H and H1. assumption. Exists_Intro with x. assumption. Impl_Intro. Not_Intro. Exists_Elim in H0. Forall_Elim in H with x. Not_Elim in H3 and H1. assumption. Qed. Lemma L65f (A : Type) (P Q : A -> Prop) : (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x). Proof. unfold iff; And_Intro. Impl_Intro. And_Intro. Forall_Intro. Forall_Elim in H with x. And_Elim_1 in H1. assumption. Forall_Intro. Forall_Elim in H with x. And_Elim_2 in H1. assumption. Impl_Intro. Forall_Intro. And_Intro. And_Elim_1 in H. Forall_Elim in H0 with x. assumption. And_Elim_2 in H. Forall_Elim in H0 with x. assumption. Qed.