From 7abef2212f0634241a57e5e8b0a65e12e94cdc13 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 1 Feb 2017 19:19:51 -0500
Subject: Add wordToZ_ZToWord_wordToZ

---
 src/Util/FixedWordSizesEquality.v | 40 ++++++++++++++++++++++++++++-----------
 1 file changed, 29 insertions(+), 11 deletions(-)

(limited to 'src/Util/FixedWordSizesEquality.v')

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.
-- 
cgit v1.2.3