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 = nHere 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.## Solution

Look at this file

Going home

Pierre Castéran