(*** Introduction to Computational Logic, Coq part of Assignment 3 ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/cl-ss11/forum/ ***) Set Implicit Arguments. Lemma AndI (X Y : Prop) : X -> Y -> X /\ Y. Proof. tauto. Qed. Lemma AndE (X Y U : Prop) : X /\ Y -> (X -> Y -> U) -> U. Proof. tauto. Qed. Goal forall X Y : Prop, X /\ Y -> Y /\ X. Proof. intros X Y A. apply (AndE A). intros x y. apply AndI. exact y. exact x. Qed. Lemma ExI (X : Type) (p : X -> Prop) : forall x : X, p x -> exists x, p x. Proof. intros x A. exists x. exact A. Qed. Lemma ExE (X : Type) (p : X -> Prop) (U : Prop) : (exists x, p x) -> (forall x, p x -> U) -> U. Proof. intros [x A] B. exact (B x A). Qed. (*** Exercise 3.2 ***) Goal forall (X : Type) (p q : X -> Prop), (exists x, p x /\ q x) -> exists x, p x. Proof. intros X p q A. apply (ExE _ A). intros x B. apply (AndE B). intros C _. apply (ExI _ x). exact C. Qed. (*** Exercise 3.3 ***) Lemma OrIL (X Y : Prop) : (*** Give Proposition and Proof ***) Lemma OrIR (X Y : Prop) : (*** Give Proposition and Proof ***) Lemma OrE (X Y U : Prop) : (*** Give Proposition and Proof ***) Goal forall X Y:Prop, X \/ Y -> Y \/ X. (*** Give Proof using OrIL, OrIR, OrE. ***) (*** Exercise 3.4 ***) Lemma EqI (X : Type) (x : X) : (*** Give Proposition and Proof ***) Lemma EqE (X : Type) (x y : X) (p : X -> Prop) : (*** Give Proposition and Proof ***) Goal forall X:Type, forall x y:X, x = y -> y = x. (*** Give Proof using EqI and EqE. ***) Goal forall X:Type, forall x y z:X, x = y -> y = z -> x = z. (*** Give Proof using EqI and EqE. ***) (*** Exercise 3.5 ***) Definition XM : Prop := forall X : Prop, X \/ ~X. Definition DN : Prop := forall X:Prop, ~~X -> X. Definition CP : Prop := forall X Y:Prop, (~Y -> ~X) -> X -> Y. Definition Peirce : Prop := forall X Y : Prop, ((X -> Y) -> X) -> X. Goal XM -> DN. (*** Give Proof ***) Goal DN -> CP. (*** Give Proof ***) Goal CP -> Peirce. (*** Give Proof ***) Goal Peirce -> XM. (*** Give Proof ***) (*** Exercise 3.6 ***) Goal forall X Y : Prop, XM -> ~(X /\ Y) -> ~X \/ ~Y. (*** Give Proof ***) Goal forall (X : Type) (p : X -> Prop), XM -> ~(forall x, p x) -> exists x, ~p x. (*** Give Proof ***) (*** Exercise 3.7 ***) Lemma Drinker (X : Type) (d : X -> Prop) : (exists x:X, x = x) -> XM -> exists x:X, d x -> forall y:X, d y. (*** Give Proof ***) (*** Exercise 3.8 ***) Goal (forall P:Prop, exists G:Prop -> Prop, forall X Y:Prop, (X /\ P -> Y) <-> (X -> G Y)) \/ ~(forall P:Prop, exists G:Prop -> Prop, forall X Y:Prop, (X /\ P -> Y) <-> (X -> G Y)). (*** Give Proof ***) Goal (forall P:Prop, exists F:Prop -> Prop, forall X Y:Prop, (X -> Y /\ P) <-> (F X -> Y)) \/ ~(forall P:Prop, exists F:Prop -> Prop, forall X Y:Prop, (X -> Y /\ P) <-> (F X -> Y)). (*** Give Proof ***) (*** Exercise 3.9 ***) (*** Give an inductive definition of negation corresponding to the given introduction rule. ***) Inductive Neg (P : Prop) : Prop := (*** Give Inductive Definition ***) (*** Prove the lemma corresponding to the elimination rule. ***) Lemma NegE (P U : Prop) : (*** Give Proposition and Proof ***) (*** Exercise 3.10 ***) (*** Give a plain definition Q. ***) Definition Q (X:Type) (p q : X -> Prop) : Prop := (*** Give Definition ***) Lemma QI (X:Type) (p q : X -> Prop) : (*** Give Proposition and Proof ***) Lemma QE (X:Type) (p q : X -> Prop) (U : Prop) : (*** Give Proposition and Proof ***) (*** Give an inductive definition Q'. ***) Inductive Q' (X:Type) (p q : X -> Prop) : Prop := (*** Give Inductive Definition ***) Lemma Q'E (X:Type) (p q : X -> Prop) (U : Prop) : (*** Give Proposition and Proof ***)