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/AddGetCarry.v | |
parent | 56bf29e5a4244d665f231b5a2602694a7414c762 (diff) |
create rewrite database for saturated operations on Z
Diffstat (limited to 'src/Util/ZUtil/AddGetCarry.v')
-rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 8 |
1 files changed, 8 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. |