ex1.v

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros P Q HP HPQ; apply HPQ, HP.
Qed.

Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
  intros P Q [HnQ HPQ] HP; apply HnQ, HPQ, HP.
Qed.

Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
  intros P Q H HnP.
  destruct H as [HP | HQ].
  - destruct HnP.
    exact HP.
  - exact HQ.
Qed.

Goal forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
  intros P Q [HP|HQ] HnP; [contradict HnP|]; assumption.
Qed.

Theorem DeMorgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
  intros P Q [HnP|HnQ] [HP HQ]; contradiction.
Qed.

Theorem DeMorgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
  intros P Q [HnP HnQ] [HP|HQ]; contradiction.
Qed.

Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
  intros P Q H; split; contradict H; [left|right]; assumption.
Qed.

Theorem NotNot_LEM : forall P : Prop, ~ ~(P \/ ~P).
Proof.
  intros P H; apply H; right; contradict H; left; assumption.
Qed.