diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 13:07:15 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-10 13:07:15 -0500 |
| commit | 0dce64bd202365541c99c0f91a51ff92fb4d4625 (patch) | |
| tree | e701db3332f67595efbd4575697a6f4f5f7e10bd /src/Util | |
| parent | 0e77d60cdc1e8c27ec256ac0d429c78a4cb3f36c (diff) | |
Hint Rewrite is section-local; move to top-level
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/WordUtil.v | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index bd3c1100b..36867958f 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -780,9 +780,6 @@ Section Bounds. assumption. Qed. - 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. intros sz x y H ?. @@ -796,9 +793,6 @@ Section Bounds. rewrite <- wordize_minus; [reflexivity|apply N.le_ge; assumption]. Qed. - 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. intros. @@ -817,9 +811,6 @@ Section Bounds. assumption. Qed. - 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. intros. @@ -831,8 +822,6 @@ Section Bounds. repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]). reflexivity. Qed. - 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. @@ -845,10 +834,23 @@ Section Bounds. repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]). reflexivity. Qed. - Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN. - Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN. End Bounds. +Hint Rewrite @wordToN_wplus using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wplus using word_util_arith : pull_wordToN. + +Hint Rewrite @wordToN_wminus using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wminus using word_util_arith : pull_wordToN. + +Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN. + +Hint Rewrite @wordToN_wand using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wand using word_util_arith : pull_wordToN. + +Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN. +Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN. + Section Updates. Local Notation bound n lower value upper := ( (0 <= lower)%Z @@ -868,7 +870,7 @@ Section Updates. (valueF value0 value1) (upperF lower0 upper0 lower1 upper1). - Local Ltac add_mono := + Local Ltac add_mono := etransitivity; [| apply Z.add_le_mono_r; eassumption]; omega. Lemma add_valid_update: forall n, @@ -906,7 +908,7 @@ Section Updates. eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]; sub_mono). Qed. - Local Ltac mul_mono := + Local Ltac mul_mono := etransitivity; [|apply Z.mul_le_mono_nonneg_r]; repeat first [ eassumption |