Here is a function of division by 2:
Fixpoint div2 (n:nat):nat:= match n with 0 => 0 | 1 => 0 | S (S p) => S (div2 p) end.
Define a similar function to compute division by 3, construct a specific induction principle to reason on this function, and use it to show that the result of division is always smaller than the argument.
Define a function rem2 similar to div2, but to compute the remainder of division by 2, use the specific induction principle associated to these function to prove the following statement:
forall n:nat, 2 * div2 n + rem2 n = n
Here are two definitions of the fibonacci function. Using a specific induction principle for the first fibonacci function, prove that the two functions return consistent values.Fixpoint fib (n:nat) : nat := match n with 0 => 1 | 1 => 1 | S ((S p) as q) => fib p + fib q end. Fixpoint fib2 (n:nat) : nat*nat := match n with 0 => (1, 1) | S p => let (v1, v2) := fib2 p in (v2, v1 + v2) end.
SolutionLook at this file