(*** Introduction to Computational Logic, Coq part of Assignment 3 ***)
(***
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 bool : Type :=
| false : bool
| true : bool.

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

Fixpoint iter (n : nat) {X : Type} (f : X -> X) (x : X) : X :=
match n with
| O => x
| S n' => f (iter n' f x)
end.

Inductive void := .

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

Definition fin (n : nat) : Type := iter n option void.

(*** Exercise 1 ***)
Lemma fin_SO (x : fin (S O)) :  x = None void.

(*** FILL THIS IN WITH A PROOF SCRIPT ***)

(*** Exercise 2 ***)
Definition tofin (x : bool) : fin (S(S O)) :=
(*** FILL THIS IN WITH A DEFINITION ***)

Definition fromfin (x : fin (S(S O))) : bool :=
(*** FILL THIS IN WITH A DEFINITION ***)

Lemma bool_fin (x : bool) : 
fromfin (tofin x) = x.

(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma fin_bool (x : fin (S(S O))) : 
tofin (fromfin x) = x.

(*** FILL THIS IN WITH A PROOF SCRIPT ***)

(*** Exercise 3 ***)
Definition tonat (x : option nat) : nat :=
(*** FILL THIS IN WITH A DEFINITION ***)

Definition fromnat (n : nat) : option nat :=
(*** FILL THIS IN WITH A DEFINITION ***)

Lemma opnat_nat (x : option nat) :
fromnat (tonat x) = x.

(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma nat_opnat (n : nat) :
tonat (fromnat n) = n.

(*** FILL THIS IN WITH A PROOF SCRIPT ***)