diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 19:50:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 19:50:22 -0400 |
| commit | 0fb8dfb5e3dd975801d56d5fca0dc2990422350a (patch) | |
| tree | 10f2a836c4ce0ba7622e2570edf9209796344cb6 /src/Util/WordUtil.v | |
| parent | ba8a8f870f6d44e71ec18b02964daa97200e8610 (diff) | |
Some work on proofs in src/Reflection/Z/Interpretations.v
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 3c52146dc..fd2e5e098 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -273,9 +273,7 @@ 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)) + (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). @@ -299,3 +297,17 @@ Proof. Admitted. Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN. + +Lemma wordToN_wand : bounds_2statement (@wand _) Z.land. +Proof. + admit. +Admitted. +Hint Rewrite @wordToN_wand using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wand using word_util_arith : pull_wordToN. + +Lemma wordToN_wor : bounds_2statement (@wor _) Z.lor. +Proof. + admit. +Admitted. +Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN. |