diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 3ccaa721..a2a2430e 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 @@ -561,6 +578,7 @@ Qed. (** To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits : *) +#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")] Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := match n return Bvector n with | 0 => Bnil @@ -670,3 +688,28 @@ 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. + +Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) : + N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k. +Proof with auto. + destruct a... + induction p; simpl; f_equal... +Qed. |