From 010851c36c6c6dbdf8adb70db3502c6f7a005132 Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@google.com>
Date: Fri, 16 Feb 2018 10:52:45 +0100
Subject: create rewrite database for saturated operations on Z

---
 src/Util/ZUtil/AddGetCarry.v | 8 ++++++++
 src/Util/ZUtil/MulSplit.v    | 2 ++
 2 files changed, 10 insertions(+)

(limited to 'src/Util/ZUtil')

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.
-- 
cgit v1.2.3