diff options
| author | Yishuai Li | 2018-07-26 13:03:15 -0400 |
|---|---|---|
| committer | Yishuai Li | 2018-07-26 13:09:08 -0400 |
| commit | 3caed4eeae1e6a561e707911aeadce739aa83da6 (patch) | |
| tree | 4f935b84aa622773abf555677d6b13094a27aaf9 | |
| parent | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (diff) | |
NArith: add sized N2Bv
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 35 |
2 files changed, 37 insertions, 0 deletions
@@ -52,6 +52,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. |