Proofs using specific induction principles

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.

Solution

 Look at this file 






Going  home  

Pierre Castéran