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
end.
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.
Proof.
intros x H; case H; intros; discriminate.
Qed.
Theorem log_domain_inv :
forall x p:nat, log_domain x -> x = S (S p)->
log_domain (S (div2 p)).
Proof.
intros x p H; case H; try (intros H'; discriminate H').
intros p' H1 H2; injection H2; intros H3;
rewrite <- H3; assumption.
Defined.