Merge PR #8169: NArith: add sized N2Bv

2 files changed, 37 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index f0327e74dc..df4a1df176 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,6 +57,8 @@ Standard Library
   Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
   want).
 
+- Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 3ccaa7211a..68a98e4292 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -517,6 +517,23 @@ Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
     | Npos p => P2Bv p
   end.
 
+Fixpoint P2Bv_sized (m : nat) (p : positive) : Bvector m :=
+  match m with
+  | O => []
+  | S m =>
+    match p with
+    | xI p => true  :: P2Bv_sized  m p
+    | xO p => false :: P2Bv_sized  m p
+    | xH   => true  :: Bvect_false m
+    end
+  end.
+
+Definition N2Bv_sized (m : nat) (n : N) : Bvector m :=
+  match n with
+  | N0     => Bvect_false m
+  | Npos p => P2Bv_sized  m p
+  end.
+
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
     | Vector.nil _ => N0
@@ -670,3 +687,21 @@ rewrite H.
 destruct a, b, (Bv2N n v1), (Bv2N n v2);
  simpl; auto.
 Qed.
+
+Lemma N2Bv_sized_Nsize (n : N) :
+  N2Bv_sized (N.size_nat n) n = N2Bv n.
+Proof with simpl; auto.
+  destruct n...
+  induction p...
+  all: rewrite IHp...
+Qed.
+
+Lemma N2Bv_sized_Bv2N (n : nat) (v : Bvector n) :
+  N2Bv_sized n (Bv2N n v) = v.
+Proof with simpl; auto.
+  induction v...
+  destruct h;
+  unfold N2Bv_sized;
+  destruct (Bv2N n v) as [|[]];
+  rewrite <- IHv...
+Qed.