proposition: Theorem pow2_log : forall n, 0 < n -> half n < 2^^(log n) <= n.
proof: Proof. intro n; generalize (le_refl n). set (k:=n) at -2. clearbody k. revert k. pattern n. apply induction; clear n. - intros n n' Hn; setoid_rewrite Hn; auto with *. - intros k Hk1 Hk2. le_elim Hk1. + destruct (nlt_0_r _ Hk1). + rewrite Hk1 in Hk2. destruct (nlt_0_r _ Hk2). - intros n IH k Hk1 Hk2. destruct (lt_ge_cases k 2) as [LT|LE]. + rewrite log_init, pow_0 by auto. rewrite <- le_succ_l, <- one_succ in Hk2. le_elim Hk2. * rewrite two_succ, <- nle_gt, le_succ_l in LT. destruct LT; auto. * rewrite <- Hk2. rewrite half_1; auto using lt_0_1, le_refl. + rewrite log_step, pow_succ by auto. rewrite two_succ, le_succ_l in LE. destruct (IH (half k)) as (IH1,IH2). * rewrite <- lt_succ_r. apply lt_le_trans with k; auto. now apply half_decrease. * apply half_nz; auto. * set (K:=2^^log (half k)) in *; clearbody K. split. -- rewrite <- le_succ_l in IH1. apply mul_le_mono_l with (p:=2) in IH1. eapply lt_le_trans; eauto. nzsimpl'. rewrite lt_succ_r. eapply le_trans; [ eapply half_lower_bound | ]. nzsimpl'; apply le_refl. -- eapply le_trans; [ | eapply half_upper_bound ]. apply mul_le_mono_l; auto. Qed.
imports: Bool RelationPairs NStrongRec