(*** Introduction to Computational Logic, Coq part of Assignment 6 ***)
(***
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 ***)
Lemma ex1a (X : Prop) : X \/ X -> X.
INSERT PROOF SCRIPT

Lemma ex1b (X Y : Prop) : ~X \/ ~Y -> ~(X /\ Y).
INSERT PROOF SCRIPT

Lemma ex1c (X Y : Prop) : ~X /\ ~Y -> ~(X \/ Y).
INSERT PROOF SCRIPT

Lemma ex1d (X Y Z : Prop) : X /\ (Y \/ Z) -> X /\ Y \/ X /\ Z.
INSERT PROOF SCRIPT

Lemma ex1e (X Y Z : Prop) : (X \/ Y) -> (X -> Z) -> (Y -> Z) -> Z.
INSERT PROOF SCRIPT

(*** Exercise 3 ***)
Lemma iff_False :  
False <-> forall Z : Prop, Z.
INSERT PROOF SCRIPT

Lemma iff_and (X Y : Prop) :
X /\ Y <-> forall Z : Prop, (X -> Y -> Z) -> Z.
INSERT PROOF SCRIPT

Lemma iff_or (X Y : Prop) :
X \/ Y <-> forall Z : Prop, (X -> Z) -> (Y -> Z) -> Z.
INSERT PROOF SCRIPT

(*** Leibniz equality ***)
Definition eql {X : Type} (x y : X) : Prop :=
forall p : X -> Prop, p y -> p x.

Lemma eql_ref {X : Type} {x : X} :
eql x x.
Proof. intros p A. exact A. Qed.

Lemma eql_sym {X : Type} {x y : X} :
eql x y -> eql y x.
Proof. intros e. pattern x.  apply e. exact eql_ref. Qed.

(*** Exercise 7 ***)
Lemma ex67 (X Y : Type) (f g : X -> Y) (x : X) :
eql f g -> eql (f x) (g x).
INSERT PROOF SCRIPT

(*** Exercise 8 ***)
Lemma ex681 (X Y : Prop) :
eql X Y -> (X <-> Y).
INSERT PROOF SCRIPT

Lemma ex682 (X : Type) (x y : X) :
eql x y <-> forall r : X -> X -> Prop, (forall z, r z z) -> r x y.
INSERT PROOF SCRIPT

(*** Exercise 9 ***)
Lemma ex691 (X : Type) (p : X -> Prop) (x y : X) :
p x -> ~ p y -> ~ eql x y.
INSERT PROOF SCRIPT

Lemma ex692 (X Y : Type) (f g : X -> Y) (x : X) :
~ eql (f x) (g x) -> ~ eql f g.
INSERT PROOF SCRIPT

(*** Exercise 10 ***)
Definition ex6101P (X : Type) (o : option X) : Prop
:= INSERT TERM

Lemma ex6101 (X : Type) (x : X) :
~ eql (Some x) None.
INSERT PROOF SCRIPT

Definition ex6102P (X : Type) (x : X) (o : option X) : X
:= INSERT TERM

Lemma ex6102 (X : Type) (x y : X) :
eql (Some x) (Some y) -> eql x y.
INSERT PROOF SCRIPT