(* 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 ? *)