Require Import Arith ZArith List. (* Write a function that computes the sum of all squares of numbers between 1 and n. Use the Function command, work on integers, but use Zabs_nat as a measure. *) (* By testing on different values, find the various numbers a b c and d, such that a * f n = b * n^3 + c * n^2 + d * n. and then prove this formula. *) (* Here are two definitions of the Fibonacci function. *) Open Scope nat_scope. Function fib1 (n : nat) : nat := match n with 0 => 0 | 1 => 1 | S ((S p) as q) => fib1 p + fib1 q end. Function fib2' (m n p : nat) {struct p} : nat := match p with 0 => m | S q => fib2' n (m + n) q end. Definition fib2 p := fib2' 0 1 p. (* Prove that fib2 is correct. *) Lemma fib2'_c : Qed. Lemma fib2_c : forall x, fib2 x = fib1 x. Qed. (* Find a simple relation between fib2' a b (S p), a b and fib1 p and fib1 (S p) prove it correct. *) Lemma fib2'_dec : forall a b p, fib2' a b (S p) = a * fib1 p + b * fib1 (S p). Qed. Lemma fib_d1 : forall p, fib1 (2*p) + fib1 p * fib1 p = 2 * fib1 p * fib1(S p). Qed. Lemma fib_d2 : forall p, fib1 (2*p+1) = fib1 p * fib1 p + fib1 (S p) * fib1 (S p). Qed. Open Scope Z_scope. Function fib_pos (p:positive) : Z*Z := match p with xH => (1, 1) | xO p => let (fibp, fibsp) := fib_pos p in (fibp * (2 * fibsp - fibp), fibp^2 + fibsp^2) | xI p => let (fibp, fibsp) := fib_pos p in (fibp^2 + fibsp^2, 2*fibp * fibsp + fibsp ^ 2) end. Lemma fix_pos_c : forall p, fib_pos p = (Z_of_nat (fib1 (nat_of_P p)), Z_of_nat (fib1 (nat_of_P (Psucc p)))). Qed.