Problem with conditional_2 proof...

gistfile1.txt

Require Import Classical.

(* 
  ¬(P ∧ Q) ⇔ (¬P ∨ ¬Q)
*)
Theorem demorgan_1: forall P Q : Prop, ~(P /\ Q) <-> (~P \/ ~Q).
Proof. intros p q. unfold iff. split.
  - intros H. apply not_and_or in H. assumption.
  - intros H. apply or_not_and in H. assumption. Qed.

(*
  ¬(P ∨ Q) ⇔ (¬P ∧ ¬Q)
*)
Theorem demorgan_2: forall P Q : Prop, ~(P \/ Q) <-> (~P /\ ~Q).
Proof. intros p q. unfold iff. split.
  - intros H. apply not_or_and in H. assumption.
  - intros H. apply and_not_or in H. assumption. Qed.

(*
  P ∧ Q ⇔ Q ∧ P
*)
Theorem commutative_1: forall P Q : Prop, P /\ Q <-> Q /\ P.
Proof. intros p q. unfold iff. split.
  - intros P_and_Q. destruct P_and_Q as [P_holds Q_holds]. split. assumption. assumption.
  - intros Q_and_P. destruct Q_and_P as [Q_holds P_holds]. split. assumption. assumption. Qed.

(*
  P ∨ Q ⇔ Q ∨ P
*)
Theorem commutative_2: forall P Q : Prop, P \/ Q <-> Q \/ P.
Proof. intros P Q. unfold iff. split.
 - intro P_or_Q. destruct P_or_Q as [P_holds | Q_holds]. right. assumption. left. assumption.
 - intro Q_or_P. destruct Q_or_P as [Q_holds | P_holds]. right. assumption. left. assumption. Qed.

(*
  (P ∧ (Q ∧ R) <-> (P ∧ Q) ∧ R)
*)
Theorem associative_1: forall P Q R : Prop, (P /\ (Q /\ R) <-> (P /\ Q) /\ R).
Proof. intros. unfold iff. split.
 - intros P_and_QR. destruct P_and_QR as [P_holds Q_and_R]. destruct Q_and_R as [Q_holds R_holds]. split.
  + split. assumption. assumption.
  + assumption.
 - intros PR_and_Q. destruct PR_and_Q as [P_and_R Q_holds]. destruct P_and_R as [P_holds R_holds]. split.
  + assumption.
  + split. assumption. assumption. Qed.

Theorem distributive_1: forall P Q R : Prop, (P /\ (Q \/ R)) <-> (P /\ Q) \/ (P /\ R).
Proof. intros. unfold iff. split.
  - intros P_and_Q_or_R. destruct P_and_Q_or_R as [P_holds Q_or_R_holds]. destruct Q_or_R_holds as [Q_holds | R_holds].
    + left. split. assumption. assumption.
    + right. split. assumption. assumption.
  - intros P_and_Q_or_P_and_R. destruct P_and_Q_or_P_and_R as [P_and_Q_holds | P_and_R]. destruct P_and_Q_holds as [P_holds Q_holds]. split.
    + assumption.
    + left. assumption.
    + destruct P_and_R as [P_holds R_holds]. split. assumption. right. assumption. Qed.

Theorem distributive_2: forall P Q R : Prop, (P \/ (Q /\ R)) <-> (P \/ Q) /\ (P \/ R).
Proof. intros. unfold iff. split.
  - intros P_or_Q_and_R. destruct P_or_Q_and_R as [ P_holds | Q_and_R_holds ]. split.
  + left. assumption.
  + left. assumption.
  + destruct Q_and_R_holds as [Q_holds P_holds]. split.
    * right. assumption.
    * right. assumption.
  - intros P_or_Q_and_P_or_R. destruct P_or_Q_and_P_or_R as [ P_or_Q P_or_R ]. destruct P_or_Q.
    + left. assumption.
    + destruct P_or_R as [P_holds | R_holds].
      * left. assumption.
      * right. split. assumption. assumption. Qed.

Theorem conditional_1: forall P Q : Prop, (P -> Q) <-> (~P \/ Q).
Proof. intros. unfold iff. split.
  - intros H. apply imply_to_or. assumption.
  - intros H. apply or_to_imply. assumption. Qed.

Theorem conditional_old: forall P Q : Prop, (P -> Q) <-> ~(P /\ ~Q).
Proof. intros. unfold iff. split.
  - tauto.
  - tauto. Qed.

Theorem conditional_2: forall P Q : Prop, (P -> Q) -> ~(P /\ ~Q).
Proof. intros P Q P_implies_Q. apply demorgan_1. right. apply imply_and_or in P_implies_Q.
  - intro not_Q.  Admitted. (* I'm stuck here *)

Theorem contrapositive: forall P Q: Prop, (P -> Q) <-> ~Q -> ~P.
Proof.
  intros P Q. unfold iff. intro H. tauto. Qed.