coqex_1

coqex_1

Coq演習 第1回

coqex_1.v

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
intros.
apply H0.
assumption.
Qed.
 
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
intros.
intro.
destruct H.
apply H.
apply H1.
assumption.
Qed.
 
Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
intros.
destruct H.
contradiction.
assumption.
Qed.
 
Theorem DeMorgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
intros.
intro.
destruct H.
apply H.
destruct H0.
assumption.
apply H.
destruct H0.
assumption.
Qed.
 
Theorem DeMorgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
intros.
intro.
destruct H.
destruct H0.
apply (H H0).
apply (H1 H0).
Qed.
 
Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros.
split.
intro.
apply H.
left.
assumption.
intro.
apply H.
right.
assumption.
Qed.
 
Theorem NotNot_LEM : forall P : Prop, ~ ~(P \/ ~P).
Proof.
intros.
intro.
apply H.
right.
intro.
apply H.
left.
assumption.
Qed.