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.