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

Set Implicit Arguments.

Inductive bool : Type :=
| false : bool
| true : bool.

Definition negb (x : bool) : bool :=
match x with
| false => true
| true => false
end.

Definition andb (x y : bool) : bool :=
match x with
| false => false
| true => y
end.

(*** Exercise 1.1 ***)
Definition orb (x y : bool) : bool :=
(*** FILL THIS IN WITH A DEFINITION ***)

Lemma ex_1_1_a (x y : bool) : negb (orb x y) = andb (negb x) (negb 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.

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

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

Fixpoint power (x n : nat) : nat :=
(*** FILL THIS IN WITH A DEFINITION ***)

Fixpoint fac (n : nat) : nat :=
(*** FILL THIS IN WITH A DEFINITION ***)

Fixpoint even (n : nat) : bool :=
(*** FILL THIS IN WITH A DEFINITION ***)

Fixpoint eq_nat (x y : nat) : bool :=
(*** FILL THIS IN WITH A DEFINITION ***)

(*** Exercise 1.4 ***)
Lemma mul_O (x:nat): mul x O = O.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma mul_S (x y:nat): mul x (S y) = add (mul x y) x.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Lemma mul_com (x y:nat): mul x y = mul y x.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

Inductive pair (X Y : Type) : Type :=
| P : X -> Y -> pair X Y.

Definition fst X Y (p : pair X Y) : X :=
match p with P x _ => x end.
Definition snd X Y (p : pair X Y) : Y :=
match p with P _ y => y end.
Compute fst (P O true).
Definition swap X Y (p : pair X Y) : pair Y X := P (snd p) (fst p).

(*** Exercise 1.5 ***)
Lemma swap_swap  (X Y : Type) (p : pair X Y) :
swap (swap p) = p.
(*** FILL THIS IN WITH A PROOF SCRIPT ***)

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

Implicit Arguments nil [X].

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

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

Fixpoint rev X (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 1.6 ***)
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 1.7 ***)
Fixpoint lengthi X (xs : list X) (a : nat) :=
match xs with
| nil => a
| cons _ xr => lengthi  xr (S a)
end.

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

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