diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-02-16 18:15:18 +0100 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-02-23 13:06:33 -0500 |
| commit | 636ba579315b8f1fadf3714097d61378e3eff528 (patch) | |
| tree | fd8b52e7df121ff7ba08ac8ed898dec8dcc24d55 /src/Util/ZUtil.v | |
| parent | b54acb5b7012a8e4540e29c68d6f10f32b88009f (diff) | |
add three proofs to ZUtil
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 973c2685d..2ff1ef834 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -964,6 +964,18 @@ Module Z. Qed. Hint Resolve div_sub_mod_cond : zarith. + Lemma div_add_mod_cond_l : forall x y d, d <> 0 -> (x + y) / d = (x mod d + y) / d + x / d. + Proof. + intros. replace (x + y) with ((x - x mod d) + (x mod d + y)) by lia. + rewrite Z.div_add_exact by auto with zarith. + rewrite <- Z.div_sub_mod_exact by lia; lia. + Qed. + + Lemma div_add_mod_cond_r : forall x y d, d <> 0 -> (x + y) / d = (x + y mod d) / d + y / d. + Proof. + intros. rewrite Z.add_comm, div_add_mod_cond_l by auto. repeat (f_equal; try ring). + Qed. + Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n. Proof. intros; Z.div_mod_to_quot_rem; nia. Qed. Hint Rewrite div_between using zutil_arith : zsimplify. |