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

Lemma iff_circuit (X : Prop) : 
~(X <-> ~X).
Proof. intros [f g]. assert (x : X). apply g. intros x. exact (f x x).
exact (f x x). Qed. 

Lemma Russell' (X : Type) (p : X -> X -> Prop) (x :X):
exists y, ~ (p x y <-> ~ p y y).
(*** INSERT PROOF SCRIPT ***)

Lemma Barber (X : Type) (m : X -> Prop) (s : X -> X -> Prop) (b :X) :
(forall x,  m x -> (s b x <-> ~ s x x)) -> ~ m b.
(*** INSERT PROOF SCRIPT ***)

Lemma GCantor (X Y : Type) (n : Y -> Y) :
(forall y, n y <> y) -> forall f : X -> X -> Y, exists g : X -> Y, forall x:X, f x <> g.
(*** INSERT PROOF SCRIPT ***)

Definition XM : Prop := forall X : Prop, X \/ ~X.
Definition DN : Prop := forall X : Prop, ~~X -> X.

Lemma DN_Contra :  DN <-> forall X Y: Prop,  (~Y -> ~X) -> X -> Y.
(*** INSERT PROOF SCRIPT USING generalize AND tauto ***)

Lemma DN_Contra' :  DN <-> forall X Y: Prop,  (~Y -> ~X) -> X -> Y.
(*** INSERT PROOF SCRIPT WITHOUT tauto ***)

Lemma XM_Contra :  XM <-> forall X Y: Prop,  (~Y -> ~X) -> X -> Y.
(*** INSERT PROOF SCRIPT USING generalize AND tauto ***)

Lemma XM_Contra' :  XM <-> forall X Y: Prop,  (~Y -> ~X) -> X -> Y.
(*** INSERT PROOF SCRIPT WITHOUT tauto ***)

Lemma DN_Peirce :  DN <-> forall X Y: Prop,  ((X -> Y) -> X) -> X.
(*** INSERT PROOF SCRIPT USING generalize AND tauto ***)

Lemma DN_Peirce' :  DN <-> forall X Y: Prop,  ((X -> Y) ->X) -> X.
(*** INSERT PROOF SCRIPT WITHOUT tauto ***)

(*** The next 3 lemmas are discussed in the lecture notes. ***)
Lemma eq_sym {X : Type} {x y : X} :
x = y -> y = x.
Proof. intros e. rewrite e. reflexivity. Qed.

Lemma f_equal {X Y : Type} (f : X -> Y) {x y : X} :
x = y -> f x = f y.
Proof. intros e. destruct e. reflexivity. Qed.

Lemma neq_False_True :  
False <> True.
intros e. rewrite e. exact I.
Qed.

Definition boolp (x : bool) : Prop := if x then True else False.

Lemma boolp_injective (x y : bool) :  boolp x = boolp y -> x = y.
(*** INSERT PROOF SCRIPT ***)

Lemma boolp_True (x : bool) :  boolp x = True -> x = true.
(*** INSERT PROOF SCRIPT ***)

Lemma negb_neq (x : bool) :  negb x <> x.
(*** INSERT PROOF SCRIPT ***)

Lemma true_or_false (x : bool) :  x=true \/ x=false.
(*** INSERT PROOF SCRIPT ***)

Lemma xor_com (x y : bool) :  (if x then negb y else y) = (if y then negb x else x).
(*** INSERT PROOF SCRIPT ***)

Lemma BCantor (X : Type) :
forall f : X -> X -> bool, exists g : X -> bool, forall x:X, f x <> g.
(*** INSERT PROOF SCRIPT ***)