Require Import Coq.Init.Prelude.
(** **
Coq is available from its website #https://coq.inria.fr/# or in a web-browser, #https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html#.
For each exercise you attempt below, delete the comment "(** fill in proof here *)" and fill in your own proof. Simply typing "tauto" will not earn you credit.
To skip an exercise, you can comment it out by adding "(**" before the statement of the theorem and "*)" after the Qed.
You'll eventually have to comment out the last theorem if you want the whole document to compile.
*)
Theorem modus_ponens (P Q : Prop) : ((P /\ (P -> Q)) -> Q).
Proof.
(** fill in proof here *)
Qed.
Theorem law_of_non_contradiction (P : Prop) : ~(P /\ (~P)).
Proof.
(** fill in proof here *)
Qed.
Theorem transitivity_of_implication (P Q R : Prop) : (((P -> Q) /\ (Q -> R)) -> (P -> R)).
Proof.
(** fill in proof here *)
Qed.
Theorem modus_tollens (P Q : Prop) : (((P -> Q) /\ ~Q) -> ~P).
Proof.
(** fill in proof here *)
Qed.
Theorem modus_ponens_reprise (P Q : Prop) : (P -> ((P -> Q) -> Q)).
Proof.
(** fill in proof here *)
Qed.
Theorem double_negation_introduction (P : Prop) : (P -> ~~P).
Proof.
(** fill in proof here *)
Qed.
Theorem DeMorgan1 (P Q : Prop) : ((~P /\ ~Q) -> ~(P \/ Q)).
Proof.
(** fill in proof here *)
Qed.
Theorem DeMorgan2 (P Q : Prop) : (~(P \/ Q) -> (~P /\ ~ Q)).
Proof.
(** fill in proof here *)
Qed.
Theorem DeMorgan (P Q : Prop) : ((~P /\ ~Q) <->~(P \/ Q)).
Proof.
(** fill in proof here; hint: use the proofs DeMorgan1 and DeMorgan2 to construct this proof.*)
Qed.
Theorem double_negation_elimination (P : Prop) : (~~P -> P).
Proof.
(** try to explain (on paper) why you can't prove this tautology similarly to the ones considered above *)
Qed.