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



Yves Bertot
Last modified: Sun May 3 13:54:06 CEST 2015