blob: 44983f6916ba49cb8b3c9147f39ceb563631f9ba (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import BinInt Zorder Zpow_def.
Local Open Scope Z_scope.
(** Definition of Zlog2 *)
Definition Zlog2 z :=
match z with
| Zpos (p~1) => Zpos (Psize_pos p)
| Zpos (p~0) => Zpos (Psize_pos p)
| _ => 0
end.
Lemma Zlog2_spec : forall n, 0 < n ->
2^(Zlog2 n) <= n < 2^(Zsucc (Zlog2 n)).
Proof.
intros [|[p|p|]|] Hn; split; try easy; unfold Zlog2;
rewrite <- ?Zpos_succ_morphism, Zpower_Ppow.
eapply Zle_trans with (Zpos (p~0)).
apply Psize_pos_le.
apply Zlt_le_weak. exact (Pcompare_p_Sp (p~0)).
apply Psize_pos_gt.
apply Psize_pos_le.
apply Psize_pos_gt.
Qed.
Lemma Zlog2_nonpos : forall n, n<=0 -> Zlog2 n = 0.
Proof.
intros [|p|p] H; trivial; now destruct H.
Qed.
|
