(*** Semantics, 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-ss11/forum/
***)

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_1b (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.

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

Definition pred (x : nat) : nat :=
match x with
| O => O
| S x' => x'
end.

(*** Exercise 1.2 ***)
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 mod3 (n : nat) : nat :=
(*** FILL THIS IN WITH A DEFINITION ***)

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.3 ***)
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 ***)

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

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