Beginning of How to Prove it proves in Coq.

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. tauto. Qed.

(*
  P ∨ Q ⇔ Q ∨ P
*)
Theorem commutative_2: forall P Q : Prop, P \/ Q <-> Q \/ P.
Proof. tauto. Qed.

(*
  (P ∧ (Q ∧ R) <-> (P ∧ Q) ∧ R)
*)
Theorem associative_1: forall P Q R : Prop, (P /\ (Q /\ R) <-> (P /\ Q) /\ R).
Proof. tauto. Qed. 

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

Theorem distributive_2: forall P Q R : Prop, (P \/ (Q /\ R)) <-> (P \/ Q) /\ (P \/ R).
Proof. intros. unfold iff. split.
  - tauto.
  - tauto. 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_2: forall P Q : Prop, (P -> Q) <-> ~(P /\ ~Q).
Proof. intros. unfold iff. split.
  - intros H. tauto. 
  - intros H. tauto. Qed.

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