diff options
author | Jason Gross <jgross@mit.edu> | 2017-02-01 19:19:51 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-02-01 19:19:51 -0500 |
commit | 7abef2212f0634241a57e5e8b0a65e12e94cdc13 (patch) | |
tree | 936dc88c440142eb6468456f8c5f3e3160b5f192 /src/Util/FixedWordSizesEquality.v | |
parent | fd0ee9c2af644628a1d059c3c000caf3c6286910 (diff) |
Add wordToZ_ZToWord_wordToZ
Diffstat (limited to 'src/Util/FixedWordSizesEquality.v')
-rw-r--r-- | src/Util/FixedWordSizesEquality.v | 40 |
1 files changed, 29 insertions, 11 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 99512f6a1..09b15eb7c 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -128,6 +128,14 @@ Proof. 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. + unfold ZToWord_gen, wordToZ_gen; intro H. + rewrite N2Z.id, wordToN_NToWord_wordToN by omega. + reflexivity. +Qed. + Lemma ZToWord_wordToZ : forall {sz} v, ZToWord (@wordToZ sz v) = v. Proof. unfold wordT, word_case in *. @@ -141,20 +149,30 @@ Proof. assumption. Qed. +Local Ltac handle_le := + 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. + 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. + handle_le. +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. + intros sz1 sz2; break_match; intros; apply wordToZ_gen_ZToWord_gen_wordToZ_gen; + handle_le. Qed. |