diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-08 11:12:21 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-08 11:12:21 -0400 |
commit | 676d72059269e349bf731968fa15070dad41b9ac (patch) | |
tree | 240f3d508e219b6b0130c67e00c9be08ea45760e /src/Util/WordUtil.v | |
parent | 7e68f242814aadf91e5b81a9f6c0a6236040b8dd (diff) |
Add ZToWord_wordToZ_ZToWord_small
Diffstat (limited to 'src/Util/WordUtil.v')
-rw-r--r-- | src/Util/WordUtil.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 4833f0df6..fc1ac28a6 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -414,6 +414,31 @@ Section WordToN. reflexivity. } } Qed. + Lemma NToWord_wordToN_NToWord_small : forall sz1 sz2 w, + (wordToN (NToWord sz2 w) < 2^N.of_nat sz1)%N + -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w. + Proof. + intros sz1 sz2 w H. + apply wbit_inj_iff_lt; intros k Hlt. + rewrite !wbit_NToWord, wordToN_testbit, wbit_NToWord, Nat2N.id. + destruct (N.eq_dec (wordToN (NToWord sz2 w)) 0) as [H'|H']; + [ apply N.bits_inj_iff in H'; specialize (H' (N.of_nat k)); + rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'; simpl in * + | assert (H'' : sz1 <= k -> N.testbit (wordToN (NToWord sz2 w)) (N.of_nat k) = false); + [ intro; + apply N.log2_lt_pow2 in H; [ | lia.. ] + | rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'' ] ]; + break_match; try reflexivity; + repeat match goal with + | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H + | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H + | _ => omega + | _ => congruence + | _ => rewrite N.bits_above_log2 by lia + | _ => solve [ symmetry; auto ] + end. + Qed. + Lemma NToWord_wordToN_NToWord : forall sz1 sz2 w, sz2 <= sz1 -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w. Proof. |