A well-specified log with recursion on an ad-hoc predicate

Define a well-specified log function by recursion on the ad-hoc predicate log_domain defined as follows:

Fixpoint two_power (n:nat) : nat :=
  match n with
  | O => 1
  | S p => 2 * two_power p

Fixpoint div2 (n:nat) : nat :=
  match n with S (S p) => S (div2 p) | _ => 0 end.
Inductive log_domain : nat->Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 :
    forall p:nat, log_domain (S (div2 p))-> log_domain (S (S p)).

The same lemmas are needed as for the exercise on a well-specified discrete log function by well-founded recursion (see this file). The following theorems will also play an important role.

Theorem log_domain_non_O : forall x:nat, log_domain x -> x <> 0.
 intros x H; case H; intros; discriminate.
Theorem log_domain_inv :
 forall x p:nat, log_domain x -> x = S (S p)-> 
            log_domain (S (div2 p)).
 intros x p H; case H; try (intros H'; discriminate H').
 intros p' H1 H2; injection H2; intros H3; 
 rewrite <- H3; assumption.


Follow this link

Going home
Yves Bertot
Last modified: Tue May 20 15:26:16 MEST 2003