(*** 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/
***)
Set Implicit Arguments.

Definition TRUE : Prop := forall X:Prop, X -> X.

Definition FALSE : Prop := forall X:Prop, X.

Definition NOT : Prop -> Prop := fun X:Prop => X -> FALSE.

Definition AND : Prop -> Prop -> Prop
 := fun X Y => forall Z:Prop, (X -> Y -> Z) -> Z.

Definition OR : Prop -> Prop -> Prop
 := fun X Y => forall Z:Prop, (X -> Z) -> (Y -> Z) -> Z.

Definition EX : forall X:Type, (X -> Prop) -> Prop
 := fun X p => forall Z:Prop, (forall x:X, p x -> Z) -> Z.

Definition EQ : forall X:Type, X -> X -> Prop
 := fun X x y => forall p:X -> Prop, p x -> p y.

(*** Exercise 6.1 ***)
Goal OR TRUE FALSE.
Proof. exact (). Qed.

Goal OR TRUE FALSE.

Goal True \/ False.

Goal NOT (EQ TRUE FALSE).
Proof. exact (). Qed.

Goal NOT (EQ TRUE FALSE).

Goal NOT (EQ false true).
Proof.
exact ().
Qed.

Goal NOT (EQ false true).

Goal false <> true.

Goal forall (p : bool -> Prop) (x : bool),
        p false -> p true -> p x.
Proof. exact (). Qed.

Goal forall (p : bool -> Prop) (x : bool),
        p false -> p true -> p x.

Goal forall (p : bool -> Prop) (x : bool),
        p false -> p true -> p (negb (negb x)).
Proof. exact (). Qed.

Goal forall (p : bool -> Prop) (x : bool),
        p false -> p true -> p (negb (negb x)).

Goal forall (p : bool -> Prop) (x:bool),
        p (negb x) -> p x -> p false.
Proof.
exact ().
Qed.

Goal forall (p : bool -> Prop) (x:bool),
        p (negb x) -> p x -> p false.

Goal forall (p : bool -> Prop) (x y : bool),
        p (negb x) -> p x -> p y.
Proof.
exact ().
Qed.

Goal forall (p : bool -> Prop) (x y : bool),
        p (negb x) -> p x -> p y.

Goal forall x : nat,
        NOT (EQ (S x) O).
Proof.
exact ().
Qed.

Goal forall x : nat,
        NOT (EQ (S x) O).

Goal forall x : nat,
        (S x) <> O.

Goal forall x y : nat,
        EQ (S x) (S y) -> EQ x y.
Proof.
exact ().
Qed.

Goal forall x y : nat,
        EQ (S x) (S y) -> EQ x y.

Goal forall x y : nat,
        S x = S y -> x = y.

Goal forall (p : nat -> Prop) (x : nat),
        p O -> (forall x, p (S x)) -> p x.
Proof.
exact ().
Qed.

Goal forall (p : nat -> Prop) (x : nat),
        p O -> (forall x, p (S x)) -> p x.

Goal forall (p : nat -> Prop) (x : nat),
        p O -> (forall x, p x -> p (S x)) -> p x.
Proof.
exact ().
Qed.

Goal forall (p : nat -> Prop) (x : nat),
        p O -> (forall x, p x -> p (S x)) -> p x.

(*** Exercise 6.2 ***)
Goal forall p : nat -> Prop, 
        p O -> p (S O) -> (forall x : nat, p x -> p (S (S x))) -> forall x : nat, p x.
Proof.
exact ().
Qed.