(*** Introduction to Computational Logic, Coq part of Assignment 2 ***)
(***
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-ss12/forum/
***)

(*** Exercise 1 ***)
Lemma eq_trans X (x y z:X) : (*** FILL IN PROPOSITION ***)
(*** FILL IN PROOF ***)

(*** Exercise 2 ***)
Goal forall X Y, (forall Z, (X -> Y -> Z) -> Z) -> X.
(*** FILL IN PROOF ***)

Goal forall X : Prop, ~~~X -> ~X.
(*** FILL IN PROOF ***)

Goal forall X Y : Prop, (X -> Y) -> ~Y -> ~X.
(*** FILL IN PROOF ***)

Goal forall X : Prop, ~(X <-> ~X).
(*** FILL IN PROOF ***)

(*** Exercise 3 ***)
Goal forall (p : bool -> Prop) (x : bool),
p true -> p false -> p x.
(*** FILL IN PROOF ***)

Goal forall (p : nat -> Prop) (x : nat),
p O -> (forall n, p n -> p (S n)) -> p x.
(*** FILL IN PROOF ***)

Goal forall (X : Type) (p : list X -> Prop) (xs : list X),
p nil -> (forall x xs, p xs -> p (cons x xs)) -> p xs.
(*** FILL IN PROOF ***)

(*** Exercise 4 ***)
Goal forall X Y : Prop,
(X -> Y) -> forall x : X, Y.
(*** FILL IN PROOF ***)

Goal forall X Y : Prop,
(forall x : X, Y) -> X -> Y.
(*** FILL IN PROOF ***)

Goal forall X Y : Prop,
(X -> Y) = (forall x : X, Y).
(*** FILL IN PROOF ***)

(*** Exercise 5 ***)
Goal forall X Y : Prop, 
X /\ (X \/ Y) <-> X.
(*** FILL IN PROOF ***)

Goal forall X Y Z : Prop, 
X /\ (Y \/ Z) <-> X /\ Y \/ X /\ Z.
(*** FILL IN PROOF ***)

(*** Exercise 6 ***)
Goal forall X Y : Prop,
~(X \/ Y) <-> ~X /\ ~Y.
(*** FILL IN PROOF ***)

Goal forall X : Type, forall p:X -> Prop,
~(exists x:X, p x) <-> forall x:X, ~p x.
(*** FILL IN PROOF ***)

(*** Exercise 7 ***)
Goal forall (X : Type) (x y : X), 
x = y <-> forall r : X -> X -> Prop, (forall z, r z z) -> r x y.
(*** FILL IN PROOF ***)

Goal forall (X : Type) (x y : X), 
x <> y <-> exists r : X -> X -> Prop, (forall z : X, r z z) /\ ~r x y.
(*** FILL IN PROOF ***)

Goal forall (X : Type) (x y : X), 
x <> y <-> exists p : X -> Prop, p x /\ ~p y.
(*** FILL IN PROOF ***)

(*** Exercise 8 ***)
Goal forall (X: Type) (p : X -> Prop) (x : X),
exists q:X -> Prop, q x /\ (forall y, p y -> q y) /\ forall y, q y -> p y \/ x = y.
(*** FILL IN PROOF ***)

(*** Exercise 9 ***)
Goal False <-> forall Z : Prop, Z.
(*** FILL IN PROOF ***)

Goal forall X : Prop, 
~X <-> forall Z : Prop, X -> Z.
(*** FILL IN PROOF ***)

Goal forall X Y : Prop, 
X /\ Y <-> forall Z  :Prop, (X -> Y -> Z) -> Z.
(*** FILL IN PROOF ***)

Goal forall X Y : Prop, 
X \/ Y <-> forall Z : Prop, (X -> Z) -> (Y -> Z) -> Z.
(*** FILL IN PROOF ***)

Goal forall (X : Type) (p : X -> Prop),
(exists x:X, p x) <-> forall Z : Prop, (forall x:X, p x -> Z) -> Z.
(*** FILL IN PROOF ***)

Goal forall (X : Type) (x y : X), 
x=y <-> forall p : X -> Prop, p x -> p y.
(*** FILL IN PROOF ***)