diff options
author | Jade Philipoom <jadep@google.com> | 2018-02-16 10:52:45 +0100 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-02-23 13:06:33 -0500 |
commit | 010851c36c6c6dbdf8adb70db3502c6f7a005132 (patch) | |
tree | 389f14014445d82eea14cbaea11293dbfc09853f /src/Util/ZUtil | |
parent | 56bf29e5a4244d665f231b5a2602694a7414c762 (diff) |
create rewrite database for saturated operations on Z
Diffstat (limited to 'src/Util/ZUtil')
-rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 8 | ||||
-rw-r--r-- | src/Util/ZUtil/MulSplit.v | 2 |
2 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index 85e9ece74..e8f8d883d 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -69,18 +69,22 @@ Module Z. Lemma add_get_carry_full_mod s x y : fst (Z.add_get_carry_full s x y) = (x + y) mod s. Proof. easypeasy. Qed. + Hint Rewrite add_get_carry_full_mod : to_div_mod. Lemma add_get_carry_full_div s x y : snd (Z.add_get_carry_full s x y) = (x + y) / s. Proof. easypeasy. Qed. + Hint Rewrite add_get_carry_full_div : to_div_mod. Lemma add_with_get_carry_full_mod s c x y : fst (Z.add_with_get_carry_full s c x y) = (c + x + y) mod s. Proof. easypeasy. Qed. + Hint Rewrite add_with_get_carry_full_mod : to_div_mod. Lemma add_with_get_carry_full_div s c x y : snd (Z.add_with_get_carry_full s c x y) = (c + x + y) / s. Proof. easypeasy. Qed. + Hint Rewrite add_with_get_carry_full_div : to_div_mod. Lemma sub_with_borrow_to_add_get_carry c x y : Z.sub_with_borrow c x y = Z.add_with_carry (-c) x (-y). @@ -89,17 +93,21 @@ Module Z. Lemma sub_get_borrow_full_mod s x y : fst (Z.sub_get_borrow_full s x y) = (x - y) mod s. Proof. easypeasy. Qed. + Hint Rewrite sub_get_borrow_full_mod : to_div_mod. Lemma sub_get_borrow_full_div s x y : snd (Z.sub_get_borrow_full s x y) = - ((x - y) / s). Proof. easypeasy. Qed. + Hint Rewrite sub_get_borrow_full_div : to_div_mod. Lemma sub_with_get_borrow_full_mod s c x y : fst (Z.sub_with_get_borrow_full s c x y) = (x - y - c) mod s. Proof. easypeasy. Qed. + Hint Rewrite sub_with_get_borrow_full_mod : to_div_mod. Lemma sub_with_get_borrow_full_div s c x y : snd (Z.sub_with_get_borrow_full s c x y) = - ((x - y - c) / s). Proof. easypeasy. Qed. + Hint Rewrite sub_with_get_borrow_full_div : to_div_mod. End Z. diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v index 1cc6b7af0..1b824a2c6 100644 --- a/src/Util/ZUtil/MulSplit.v +++ b/src/Util/ZUtil/MulSplit.v @@ -21,9 +21,11 @@ Module Z. unfold Z.mul_split; break_match; Z.ltb_to_lt; [ rewrite mul_split_at_bitwidth_mod; congruence | reflexivity ]. Qed. + Hint Rewrite mul_split_mod : to_div_mod. Lemma mul_split_div s x y : snd (Z.mul_split s x y) = (x * y) / s. Proof. unfold Z.mul_split; break_match; Z.ltb_to_lt; [ rewrite mul_split_at_bitwidth_div; congruence | reflexivity ]. Qed. + Hint Rewrite mul_split_div : to_div_mod. End Z. |