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/FixedWordSizesEquality.v | |
parent | 7e68f242814aadf91e5b81a9f6c0a6236040b8dd (diff) |
Add ZToWord_wordToZ_ZToWord_small
Diffstat (limited to 'src/Util/FixedWordSizesEquality.v')
-rw-r--r-- | src/Util/FixedWordSizesEquality.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index e1a8f1f79..c8f37c86b 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -129,6 +129,18 @@ Proof. reflexivity. Qed. +Lemma ZToWord_gen_wordToZ_gen_ZToWord_gen_small : forall {sz1 sz2} v, + (wordToZ_gen (@ZToWord_gen sz2 v) < 2^(Z.of_nat sz1))%Z + -> @ZToWord_gen sz2 (wordToZ_gen (@ZToWord_gen sz1 v)) = ZToWord_gen v. +Proof. + unfold ZToWord_gen, wordToZ_gen. + intros sz1 sz2 v H. + change 2%Z with (Z.of_nat 2) in H. + rewrite <- !nat_N_Z, <- N2Z.inj_pow, <- N2Z.inj_lt in H. + rewrite N2Z.id, NToWord_wordToN_NToWord_small by assumption. + reflexivity. +Qed. + Lemma wordToZ_gen_ZToWord_gen_wordToZ_gen sz1 sz2 w : (sz1 <= sz2)%nat -> wordToZ_gen (@ZToWord_gen sz2 (@wordToZ_gen sz1 w)) = wordToZ_gen w. Proof. @@ -171,6 +183,14 @@ Proof. handle_le. Qed. +Lemma ZToWord_wordToZ_ZToWord_small : forall {sz1 sz2} v, + (wordToZ (@ZToWord sz2 v) < 2^Z.of_nat (2^sz1))%Z -> @ZToWord sz2 (wordToZ (@ZToWord sz1 v)) = ZToWord v. +Proof. + unfold wordToZ, ZToWord, word_case_dep. + intros sz1 sz2; break_match; intros; apply ZToWord_gen_wordToZ_gen_ZToWord_gen_small; + handle_le; try omega. +Qed. + Lemma wordToZ_ZToWord_wordToZ : forall sz1 sz2 w, (sz1 <= sz2)%nat -> wordToZ (@ZToWord sz2 (@wordToZ sz1 w)) = wordToZ w. Proof. unfold wordToZ, ZToWord, word_case_dep. |