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

(*** Exercise 1 ***)
Check INSERT_PROOF_HERE
 : (forall X Y:Prop, X -> (X -> Y) -> Y).

Lemma ex1a (X Y : Prop) : X -> (X -> Y) -> Y.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall X Y:Prop, (X -> X -> Y) -> X -> Y).

Lemma ex1b (X Y : Prop) : (X -> X -> Y) -> X -> Y.
Proof.
INSERT PROOF SCRIPT
Qed.

Lemma ex1c (X Y Z : Prop) : (X -> Y -> Z) -> (X -> Y) -> X -> Z.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall X Y Z:Prop, (X -> Y -> Z) -> (X -> Y) -> X -> Z).

Lemma ex1d (X Y : Prop) : X -> Y -> forall Z:Prop, (X -> Y -> Z) -> Z.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall X Y:Prop, X -> Y -> forall Z:Prop, (X -> Y -> Z) -> Z).

Check INSERT_PROOF_HERE
 : (forall X Y:Prop, (forall Z:Prop, (X -> Y -> Z) -> Z) -> X).

Lemma ex1e (X Y:Prop) : (forall Z:Prop, (X -> Y -> Z) -> Z) -> X.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall X:Prop, forall Y:Prop, X -> forall Z:Prop, (X -> Z) -> (Y -> Z) -> Z).

Lemma ex1f (X Y:Prop) : X -> forall Z:Prop, (X -> Z) -> (Y -> Z) -> Z.
Proof.
INSERT PROOF SCRIPT
Qed.

(*** Exercise 2 ***)
Lemma ex2a : ~~~False.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (~~~False).

Check INSERT_PROOF_HERE
 : (forall X:Prop, X -> ~~X).

Lemma ex2b (X : Prop) : X -> ~~X.
Proof.
INSERT PROOF SCRIPT
Qed.

Lemma ex2c (X : Prop) : ~~~X -> ~X.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall X:Prop, ~~~X -> ~X).

Lemma ex2d (X : Prop) : ~X -> (~X -> X) -> False.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall X:Prop, ~X -> (~X -> X) -> False).

(*** Exercises 4 and 5 ***)
Lemma circuit (X : Prop) : (X -> ~X) -> (~X -> X) -> False.
Proof. intros f g. apply f. 
apply g. intros x. exact (f x x).
apply g. intros x. exact (f x x). Defined.

Print circuit.

Compute circuit.

Lemma R {X Y : Prop} :
(X -> X -> Y) -> X -> Y.
Proof. intros f x. exact (f x x). Defined.

Lemma circuit2 (X : Prop) : (X -> ~X) -> (~X -> X) -> False.
Proof. intros f g. exact (R f (g (R f))). Defined.

Print circuit2.

Compute circuit2.

Lemma test : circuit = circuit2.
Proof.
INSERT PROOF SCRIPT
Qed.

(*** Exercise 6 ***)
(*** Hint: You may want to use assert (z:False). ***)
Lemma ex6 (X Y : Prop) : ~X -> ((X -> Y) -> X) -> False.
Proof.
INSERT PROOF SCRIPT
Qed.

Print ex6.

(*** Exercise 7 ***)

Lemma ex7a (A : Type) (z : A) (r : A -> A -> Prop) : (forall x:A, forall y:A, r x y) -> r z z.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall A:Type, forall z:A, forall r:A -> A -> Prop, (forall x:A, forall y:A, r x y) -> r z z).

Lemma ex7b (A : Type) (x y : A) (q : A -> Prop) : q x -> (forall p:A -> Prop, p x -> p y) -> q y.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall A:Type, forall x:A, forall y:A, forall q:A -> Prop, q x -> (forall p:A -> Prop, p x -> p y) -> q y).

Lemma ex7c (A : Type) (x y : A) (q : A -> Prop) : q y -> (forall p:A -> Prop, p x -> p y) -> q x.
Proof.
INSERT PROOF SCRIPT
Qed.

Check INSERT_PROOF_HERE
 : (forall A:Type, forall x:A, forall y:A, forall q:A -> Prop, q y -> (forall p:A -> Prop, p x -> p y) -> q x).