Skip to content

Instantly share code, notes, and snippets.

@KeenS

KeenS/1-4.v

Created April 7, 2014 14:15
Show Gist options
  • Save KeenS/10021119 to your computer and use it in GitHub Desktop.
Save KeenS/10021119 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
1-4.v
Theorem DeBolran1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
intros.
destruct H.
intro.
destruct H0.
apply H, H0.
intro.
destruct H.
destruct H0.
apply H0.
Qed.
Theorem DeBolran2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
intros.
destruct H.
intro.
destruct H1.
apply H, H1.
apply H0, H1.
Qed.
Theorem DeBolran3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros.
split.
intro.
destruct H.
left.
apply H0.
intro.
destruct H.
right.
apply H0.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment