From fd0ee9c2af644628a1d059c3c000caf3c6286910 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 1 Feb 2017 18:40:54 -0500 Subject: Add ZToWord_wordToZ_ZToWord --- src/Util/FixedWordSizesEquality.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'src/Util/FixedWordSizesEquality.v') diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 00f232d50..99512f6a1 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -119,6 +119,15 @@ Proof. assumption. Qed. +Lemma ZToWord_gen_wordToZ_gen_ZToWord_gen : forall {sz1 sz2} v, + (sz2 <= sz1)%nat -> @ZToWord_gen sz2 (wordToZ_gen (@ZToWord_gen sz1 v)) = ZToWord_gen v. +Proof. + unfold ZToWord_gen, wordToZ_gen. + intros sz1 sz2 v H. + rewrite N2Z.id, NToWord_wordToN_NToWord by omega. + reflexivity. +Qed. + Lemma ZToWord_wordToZ : forall {sz} v, ZToWord (@wordToZ sz v) = v. Proof. unfold wordT, word_case in *. @@ -131,3 +140,21 @@ Proof. intros; break_match; apply wordToZ_gen_ZToWord_gen; assumption. Qed. + +Lemma ZToWord_wordToZ_ZToWord : forall {sz1 sz2} v, + (sz2 <= sz1)%nat -> @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; + repeat match goal with + | [ |- (S ?a <= 2^?b)%nat ] + => change (2^(Nat.log2 (S a)) <= 2^b)%nat + | [ |- (2^_ <= 2^_)%nat ] + => apply Nat.pow_le_mono_r + | [ |- _ <> _ ] => intro; omega + | _ => assumption + | [ |- (_ <= S _)%nat ] + => apply Nat.leb_le; vm_compute; reflexivity + | _ => exfalso; omega + end. +Qed. -- cgit v1.2.3