gistfile1.v

Theorem and_assoc: forall P Q R:Prop, ((P /\ Q) /\ R) -> (P /\ (Q /\ R)).
Proof.
intros.
destruct H.
split.
destruct H.
exact H.
destruct H. 
split.
exact H1.
exact H0.
Qed. 

Theorem or_assoc: forall P Q R:Prop, ((P \/ Q) \/ R) -> (P \/ (Q \/ R)).
Proof.
intros.
destruct H.
destruct H.
left.
exact H.
right.
left.
exact H.
right.
right.
exact H.
Qed.

Theorem and_or_dist: forall P Q R:Prop, ((P /\ Q) \/ R) -> (P \/ R) /\ (Q \/ R).
Proof.
intros.
destruct H.
split.
destruct H.
left.
exact H.
destruct H.
left.
exact H0.
split.
right.
exact H.
right.
exact H.
Qed.

Theorem or_and_dist: forall P Q R:Prop, ((P \/ Q) /\ R) -> (P /\ R) \/ (Q /\ R).
Proof.
intros.
destruct H.
destruct H.
left.
split.
exact H.
exact H0.
right.
split.
exact H.
exact H0.
Qed.

Theorem de_morgan_1: forall P Q:Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
intros.
destruct H.
intro.
apply H.
destruct H1.
apply H1.
apply H0 in H1.
destruct H.
destruct H0.
destruct H1.
Qed.

Theorem de_morgan_2: forall P Q:Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros.
split.
intro.
apply H.
left.
exact H0.
intro.
destruct H.
right.
exact H0.
Qed.

Theorem de_morgan_3: forall P Q:Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
intros.
intro.
destruct H.
apply H.
destruct H0.
exact H0.
destruct H.
destruct H0.
exact H0.
Qed.