On nested recursion

Complete the missing parts:
Require Import Arith.
Require Import Omega.

Fixpoint div2 (n:nat) : nat := match n with S (S p) => S (div2 p) | _ => 0 end.

(* as we advised in chapter 9, we use a specific induction principle
   to reason on the division function. *)

Theorem div2_ind :
 forall P:nat->Prop,
   P 0 -> P 1 -> (forall n, P n -> P (S (S n))) ->
   forall n, P n.
Proof.
 intros.
 assert (H' : P n /\ P (S n)).
 elim n; intuition.
 intuition.
Qed.

(* Once the induction principle breaks down the problem into the
   various cases, the omega tactic can handle them. *)

Theorem double_div2_le : forall x:nat, div2 x + div2 x <= x.

Theorem f_lemma : forall x v, v <= div2 x -> div2 x + v <= x.




Solution

This file
Going home
Yves Bertot
Last modified: Tue May 20 15:20:10 MEST 2003