(*** Introduction to Computational Logic, Coq part of Assignment 2 ***)
(***
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 pair (X Y : Type) : Type :=
| P : X -> Y -> pair X Y.

Implicit Arguments P [X Y].

Definition fst {X Y : Type} (p : pair X Y) : X :=
match p with P x _ => x end.
Definition snd {X Y : Type} (p : pair X Y) : Y :=
match p with P _ y => y end.

(*** Exercise 1 ***)
Definition car {X Y Z :Type} (f : X -> Y -> Z) (p : pair X Y) : Z :=
(*** FILL THIS IN WITH A DEFINITION ***)
Definition cas {X Y Z :Type}  (f : pair X Y -> Z) (x : X) (y : Y) : Z :=
(*** FILL THIS IN WITH A DEFINITION ***)
Lemma car_P (X Y Z :Type)  (f : X -> Y -> Z) (x :X) (y :Y) :
car f (P x y) = f x y.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)
Lemma cas_P (X Y Z :Type)  (f : pair X Y -> Z) (x :X) (y :Y) :
cas f x y = f (P x y).
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

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.

Lemma add_O (x : nat) : 
add x O = x.
Proof.
induction x ; simpl.
reflexivity. 
rewrite IHx. reflexivity.
Qed.

Lemma add_S (x y : nat) : 
add x (S y) = S (add x y).
Proof.
induction x ; simpl.
reflexivity. 
rewrite IHx. reflexivity.
Qed. 

Lemma add_com (x y : nat) : 
add x y = add y x.
Proof.
induction x ; simpl.
rewrite add_O. reflexivity.
rewrite add_S.  rewrite IHx. reflexivity.
Qed.

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

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.

(*** Exercise 2 ***)
Lemma iter_mul (x y : nat) :
mul x y = iter x (add y) O.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

(*** Exercise 3 ***)
Lemma iter_move (X : Type) (f : X -> X) (x : X) (n : nat) :
iter (S n) f x = iter n f (f x).
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Inductive list (X : Type) :=
| nil : list X
| cons : X -> list X -> list X.

Implicit Arguments nil [X].
Implicit Arguments cons [X].

Fixpoint length {X : Type} (xs : list X) : nat :=
match xs with
| nil => O
| cons _ xr => S (length xr)
end.

Fixpoint app {X : Type} (xs ys : list X) : list X :=
match xs with
| nil => ys
| cons x xr => cons x (app xr ys)
end.

Fixpoint rev  {X : Type} (xs : list X) : list X :=
match xs with
| nil => nil
| cons x xr => app (rev xr) (cons x nil)
end.

Lemma app_nil (X : Type) (xs : list X) :
app xs nil = xs.
Proof.
induction xs ; simpl. reflexivity. rewrite IHxs. reflexivity.
Qed.

(*** Exercise 4 ***)
Lemma app_asso (X : Type) (xs ys zs : list X) :  
app (app xs ys) zs = app xs (app ys zs).
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma length_app (X : Type) (xs ys : list X) :
length (app xs ys) = add (length xs) (length ys).
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma rev_app (X : Type) (xs ys : list X) :
rev (app xs ys) = app (rev ys) (rev xs).
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma rev_rev (X : Type) (xs : list X) :  
rev (rev xs) = xs.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

(*** Exercise 5 ***)
Fixpoint lengthi {X : Type} (xs : list X) (a : nat) :=
match xs with
| nil => a
| cons _ xr => lengthi  xr (S a)
end.

Lemma lengthi_length  {X : Type} (xs : list X) (a : nat) :
lengthi xs a = add (length xs) a.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma length_lengthi  {X : Type} (xs : list X) :
length xs = lengthi xs O.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)