diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-13 18:46:52 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-13 18:46:52 -0400 |
| commit | c22b3c9726aa1c052fd44bcaf0ced8fb30970206 (patch) | |
| tree | 4937a0d4d71ba5d3bdffb4dd16341a83917f6182 /src/Util/ZUtil | |
| parent | cd24907d7c46ddc52989a5cfa7a10c3c4568eee3 (diff) | |
Fix split_bounds, prove it correct
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Div.v | 4 | ||||
| -rw-r--r-- | src/Util/ZUtil/Modulo.v | 5 |
2 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index a9fc4aae0..5ae17ad1a 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -258,4 +258,8 @@ Module Z. intros; subst; auto with zarith. Qed. Hint Resolve div_same' : zarith. + + Lemma div_opp_r a b : a / (-b) = ((-a) / b). + Proof. Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve div_opp_r : zarith. End Z. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 8dea71870..84917a454 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -4,6 +4,7 @@ Require Import Crypto.Util.ZUtil.ZSimplify.Core. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Div. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Local Open Scope Z_scope. @@ -282,4 +283,8 @@ Module Z. autorewrite with zsimplify_const. reflexivity. Qed. + + Lemma mod_opp_r a b : a mod (-b) = -((-a) mod b). + Proof. pose proof (Z.div_opp_r a b); Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve mod_opp_r : zarith. End Z. |