From 0fb8dfb5e3dd975801d56d5fca0dc2990422350a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Oct 2016 19:50:22 -0400 Subject: Some work on proofs in src/Reflection/Z/Interpretations.v --- src/Util/WordUtil.v | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'src/Util/WordUtil.v') 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. -- cgit v1.2.3