diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-17 21:58:47 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-17 21:58:47 -0400 |
commit | c37d285157b0c6e7f442956a81ee8bd23bada251 (patch) | |
tree | 920ab26b5e1d927acd1699ece405e34819b91efe /src/Util/FixedWordSizesEquality.v | |
parent | 78a236f14d1e64f12719154947725a53a48262c9 (diff) |
Add eq_ZToWord
Diffstat (limited to 'src/Util/FixedWordSizesEquality.v')
-rw-r--r-- | src/Util/FixedWordSizesEquality.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 56c7debf6..f699adeed 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -188,6 +188,18 @@ Proof. reflexivity. Qed. +Lemma eq_ZToWord_gen : forall {sz} v1 v2, (Z.max 0 v1 mod 2^Z.of_nat sz = Z.max 0 v2 mod 2^Z.of_nat sz)%Z + <-> @ZToWord_gen sz v1 = @ZToWord_gen sz v2. +Proof. + intros; split; intro H. + { rewrite <- (ZToWord_gen_wordToZ_gen (ZToWord_gen v1)), <- (ZToWord_gen_wordToZ_gen (ZToWord_gen v2)). + rewrite !wordToZ_gen_ZToWord_gen_mod_full. + congruence. } + { apply (f_equal wordToZ_gen) in H; revert H. + rewrite !wordToZ_gen_ZToWord_gen_mod_full. + trivial. } +Qed. + Lemma ZToWord_wordToZ : forall {sz} v, ZToWord (@wordToZ sz v) = v. Proof. unfold wordT, word_case in *. @@ -262,6 +274,13 @@ Proof. intros sz w; break_match; apply wordToZ_gen_ZToWord_gen_mod_full. Qed. +Lemma eq_ZToWord : forall {sz} v1 v2, (Z.max 0 v1 mod 2^Z.of_nat (2^sz) = Z.max 0 v2 mod 2^Z.of_nat (2^sz))%Z + <-> @ZToWord sz v1 = @ZToWord sz v2. +Proof. + unfold ZToWord, word_case_dep. + intros sz v1 v2; break_innermost_match; apply eq_ZToWord_gen. +Qed. + Local Ltac wordToZ_word_case_dep_t := let H := fresh in intro H; |