(* MGS 08 : COQ 1st exercise Complete the follwoing proofs *without* using automatic tactics like auto, tauto, firstorder or ring *) Section PL. Variables P Q R : Prop. Lemma e1 : P /\ Q -> P. Lemma e2 : P -> P \/ Q. Lemma e3 : P /\ (P -> Q) -> Q. Lemma e4 : (P -> Q) -> ~Q -> ~P. Lemma e5 : (P \/ Q -> R) -> (P -> R). Lemma e6 : (P \/ Q) /\ ~P -> Q. Lemma e7 : P /\ Q -> R <-> P -> Q -> R. Lemma e8 : ~(P \/ Q) <-> ~P /\ ~Q. Lemma e9 : ~~ (P \/~P). End PL. Section QL. (* We assume as given a set and a relation. *) Variable D:Set. Variable R : D -> D -> Prop. (* We assume that the relation is transitive, reflexive and total. *) Hypothesis trans_R : forall x y z:D,R x y -> R y z -> R x z. Hypothesis sym_R : forall x y:D,R x y -> R y x. Hypothesis total_R : forall x:D,exists y:D, R x y. (* The goal is to show that R is reflexive. *) Theorem refl_R : forall x:D,R x x. End QL. Section Algebra. Require Import Arith. Lemma eq : forall a b c:nat, a+b+c = c+b+a.