Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index cb6030e26..988a9d0d3 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -255,6 +255,15 @@ Definition Pdiv2 (z:positive) :=
 
 Infix "/" := Pdiv2 : positive_scope.
 
+(** Division by 2 rounded up *)
+
+Definition Pdiv2_up p :=
+ match p with
+   | 1 => 1
+   | p~0 => p
+   | p~1 => Psucc p
+ end.
+
 (** Number of digits in a positive number *)
 
 Fixpoint Psize (p:positive) : nat :=
@@ -1292,6 +1301,17 @@ Proof.
  apply Plt_trans with (p+q); auto using Plt_plus_r.
 Qed.
 
+Lemma Ppow_gt_1 : forall n p, 1<n -> 1<n^p.
+Proof.
+ intros n p Hn.
+ induction p using Pind.
+ now rewrite Ppow_1_r.
+ rewrite Ppow_succ_r.
+ apply Plt_trans with (n*1).
+ now rewrite Pmult_1_r.
+ now apply Pmult_lt_mono_l.
+Qed.
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)