diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-27 19:40:38 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-27 19:40:38 -0400 |
commit | ba8a8f870f6d44e71ec18b02964daa97200e8610 (patch) | |
tree | f6d99a3c5f55e85f77280e4034ac7c0a5a33d7e7 /src/Util/WordUtil.v | |
parent | cf7c7901d5c9ab3623537087cd98e204d703ac27 (diff) |
Add some rewrites and admitted lemmas
Diffstat (limited to 'src/Util/WordUtil.v')
-rw-r--r-- | src/Util/WordUtil.v | 31 |
1 files changed, 31 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. |