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

Inductive nat :=
| O : nat
| S : nat -> nat.

Fixpoint add (x y : nat) : nat :=
match x with
| O => y
| S x' => S (add x' y)
end.

Inductive option (X : Type) :=
| None : option X
| Some : X -> option X.
Implicit Arguments None [X].
Implicit Arguments Some [X].

(*** Exercise 1 ***)
Definition pred' : nat -> option nat :=
(*** FILL THIS IN WITH A DEFINITION ***)

Theorem pred'O : pred' O = None.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)
Qed.

Theorem pred'S (n : nat) : pred' (S n) = Some n.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)
Qed.

(*** Exercise 2 ***)
Definition addf :=
(*** FILL THIS IN WITH A DEFINITION ***)

Theorem add_addf (x y:nat) : add x y = addf x y.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

(*** Exercise 3 ***)
Section Ex3.

Variable push : nat -> nat.
Variable pusheq : forall x,  push x = S (push x).

Definition bogus : nat  :=
(*** FILL THIS IN WITH A DEFINITION ***)

Lemma contradiction : S bogus = bogus.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

End Ex3.

(*** Exercise 4 ***)
Definition d : nat -> nat
 := fix f (x : nat) : nat := match x return nat with O => x | S y => S (S (f y)) end.
Compute (d O).
(*** LIST ALL THE REDUCTION STEPS ***)

Compute (d (S O)).
(*** LIST ALL THE REDUCTION STEPS ***)

Compute (fun z : nat => d z).
(*** LIST ALL THE REDUCTION STEPS ***)

Compute (fun z : nat => d (S z)).
(*** LIST ALL THE REDUCTION STEPS ***)