(* MGS 08 : COQ

3rd exercise

*)

Section Ex3.

Require Import Arith.

Fixpoint sum (n:nat) {struct n} : nat :=
(* Define a function which calculates the sum of the first n numbers *)

Eval compute in sum 10. (* = 55 *)

Lemma gauss_lem : forall n:nat, 2 * (sum n) = n * (n + 1).
(* Proof Gauss' theorem *)

(* Define binary numbers *)

Require Import List.

Definition bin := list bool.
Definition b0 : bin := false::nil.

Fixpoint bS (bs:bin) :bin :=
(* Define binary successor *)

Eval compute in bS(bS(bS b0)).

Fixpoint nat2bin (n:nat) : bin :=
(* define translation from nat to bin *)

Eval compute in nat2bin 25.

Fixpoint bin2nat (bs:bin) : nat :=
(* Define translation from bin to nat *)

(* A test shows that bin2nat is the inverse of bin2nat. *)
Eval compute in bin2nat (nat2bin 25). 

Theorem nat2nat : forall n:nat,bin2nat (nat2bin n) = n.
(* Proof it ! 
   You will need a lemma, use the "hypothesize first" technique.
*)

(* What about the translations the other way around:
   forall bs:bin,nat2bin(bin2nat bs) = bs ?
 *)