Add some rewrites and admitted lemmas

2 files changed, 36 insertions, 0 deletions

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index de5cd0847..3c52146dc 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -15,6 +15,8 @@ Create HintDb push_wordToN discriminated.
 Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN.
 Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN.
 
+Ltac word_util_arith := omega.
+
 Lemma pow2_id : forall n, pow2 n = 2 ^ n.
 Proof.
   induction n; intros; simpl; auto.
@@ -268,3 +270,32 @@ Proof.
            | [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst
            end.
 Qed.
+
+Local Notation bounds_2statement wop Zop
+  := (forall {sz} (x y : word sz),
+         (Z.log2 (Z.of_N (wordToN x)) < Z.of_nat sz
+          -> Z.log2 (Z.of_N (wordToN y)) < Z.of_nat sz
+          -> 0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))
+          -> Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz
+          -> Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))))%Z).
+
+Lemma wordToN_wplus : bounds_2statement (@wplus _) Z.add.
+Proof.
+  admit.
+Admitted.
+Hint Rewrite @wordToN_wplus using word_util_arith : push_wordToN.
+Hint Rewrite <- @wordToN_wplus using word_util_arith : pull_wordToN.
+
+Lemma wordToN_wminus : bounds_2statement (@wminus _) Z.sub.
+Proof.
+  admit.
+Admitted.
+Hint Rewrite @wordToN_wminus using word_util_arith : push_wordToN.
+Hint Rewrite <- @wordToN_wminus using word_util_arith : pull_wordToN.
+
+Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul.
+Proof.
+  admit.
+Admitted.
+Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN.
+Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 852803638..c5a2ae99d 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -77,6 +77,8 @@ Create HintDb pull_Zshift discriminated.
 Create HintDb push_Zshift discriminated.
 Create HintDb pull_Zof_N discriminated.
 Create HintDb push_Zof_N discriminated.
+Create HintDb pull_Zto_N discriminated.
+Create HintDb push_Zto_N discriminated.
 Create HintDb Zshift_to_pow discriminated.
 Create HintDb Zpow_to_shift discriminated.
 Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp.
@@ -101,6 +103,8 @@ Hint Extern 1 => autorewrite with Zshift_to_pow in * : Zshift_to_pow.
 Hint Extern 1 => autorewrite with Zpow_to_shift in * : Zpow_to_shift.
 Hint Extern 1 => autorewrite with pull_Zof_N in * : pull_Zof_N.
 Hint Extern 1 => autorewrite with push_Zof_N in * : push_Zof_N.
+Hint Extern 1 => autorewrite with pull_Zto_N in * : pull_Zto_N.
+Hint Extern 1 => autorewrite with push_Zto_N in * : push_Zto_N.
 Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using zutil_arith : pull_Zopp.
 Hint Rewrite Z.mul_opp_l : pull_Zopp.
 Hint Rewrite <- Z.opp_add_distr : pull_Zopp.
@@ -119,6 +123,7 @@ Hint Rewrite Z_mod_nz_opp_full using zutil_arith : push_Zmod.
 Hint Rewrite Z_mod_same_full : push_Zmod.
 Hint Rewrite Nat2Z.id N2Z.id : zsimplify.
 Hint Rewrite Nat2Z.id : push_Zof_nat.
+Hint Rewrite N2Z.id : push_Zto_N.
 Hint Rewrite N2Z.id : pull_Zof_N.
 Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 : push_Zof_N.
 Hint Rewrite N2Z.inj_compare N2Z.inj_testbit : pull_Zof_N.