# 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
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.

## Solution

Follow this link

Going home

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