Merge PR #8815: NArith: add lemmas about numbers and vectors

4 files changed, 53 insertions, 2 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 141e0c2333..faf11b9a9e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -38,6 +38,11 @@ Tools
 - A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether
   conversion can use the VM. The default value is `yes`.
 
+Standard Library
+
+- Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about
+  the upper bound of number represented by a vector.
+  Allowed implicit vector length argument in `Ndigits.Bv2N`.
 
 Changes from 8.8.2 to 8.9+beta1
 ===============================
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 92c124ec32..d319ed1029 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -422,6 +422,25 @@ Proof.
  unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H.
 Qed.
 
+Lemma double_lt_mono n m : n < m -> double n < double m.
+Proof.
+  destruct n as [|n], m as [|m]; intros H; try easy.
+Qed.
+
+Lemma double_le_mono n m : n <= m -> double n <= double m.
+Proof.
+  destruct n as [|n], m as [|m]; intros H; try easy.
+Qed.
+
+Lemma succ_double_lt_mono n m : n < m -> succ_double n < succ_double m.
+Proof.
+  destruct n as [|n], m as [|m]; intros H; try easy.
+Qed.
+
+Lemma succ_double_le_mono n m : n <= m -> succ_double n <= succ_double m.
+Proof.
+  destruct n as [|n], m as [|m]; intros H; try easy.
+Qed.
 
 (** 0 is the least natural number *)
 
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index a2a2430e91..fb1cef1ddd 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -8,9 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat.
+Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat
+        Basics ByteVector.
 
 Local Open Scope N_scope.
+Local Open Scope program_scope.
 
 (** This file is mostly obsolete, see directly [BinNat] now. *)
 
@@ -534,6 +536,9 @@ Definition N2Bv_sized (m : nat) (n : N) : Bvector m :=
   | Npos p => P2Bv_sized  m p
   end.
 
+Definition N2ByteV_sized (m : nat) : N -> ByteVector m :=
+  of_Bvector ∘ N2Bv_sized (m * 8).
+
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
     | Vector.nil _ => N0
@@ -541,6 +546,11 @@ Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
     | Vector.cons _ true n bv => N.succ_double (Bv2N n bv)
   end.
 
+Arguments Bv2N {n} bv, n bv.
+
+Definition ByteV2N {n : nat} : ByteVector n -> N :=
+  Bv2N ∘ to_Bvector.
+
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
 Proof.
 destruct n.
@@ -575,6 +585,23 @@ destruct a ; compute ; split ; intros x ; now inversion x.
   simpl ;intuition ; try discriminate.
 Qed.
 
+Lemma Bv2N_upper_bound (n : nat) (bv : Bvector n) :
+    (Bv2N bv < N.shiftl_nat 1 n)%N.
+Proof with simpl; auto.
+  induction bv...
+  - constructor.
+  - destruct h.
+    + apply N.succ_double_lt...
+    + apply N.double_lt_mono...
+Qed.
+
+Corollary ByteV2N_upper_bound (n : nat) (v : ByteVector n) :
+  (ByteV2N v < N.shiftl_nat 1 (n * 8))%N.
+Proof.
+  unfold ByteV2N, compose.
+  apply Bv2N_upper_bound.
+Qed.
+
 (** To state nonetheless a second result about composition of
  conversions, we define a conversion on a given number of bits : *)
 
diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v
index 16f26002d2..3588aaca3f 100644
--- a/theories/Strings/ByteVector.v
+++ b/theories/Strings/ByteVector.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Ascii Basics Bvector Psatz String Vector.
+Require Import Ascii Basics Bvector String Vector.
 Export VectorNotations.
 Open Scope program_scope.
 Open Scope string_scope.