From c37d285157b0c6e7f442956a81ee8bd23bada251 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 17 Jun 2017 21:58:47 -0400 Subject: Add eq_ZToWord --- src/Util/FixedWordSizesEquality.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'src/Util/FixedWordSizesEquality.v') 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; -- cgit v1.2.3