diff options
author | Jade Philipoom <jadep@google.com> | 2018-02-19 10:30:41 +0100 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-02-23 13:06:33 -0500 |
commit | 1c6e5be51dac164ccbc164f95de783277b9a6053 (patch) | |
tree | c321960fe71c6a94ce0d86cff1a2c86d812ee5fa /src/Util/ZUtil/Div.v | |
parent | 83b8293fa1cd24383fe19f51863409c37e501502 (diff) |
move things from ZUtil.v into Div.v
Diffstat (limited to 'src/Util/ZUtil/Div.v')
-rw-r--r-- | src/Util/ZUtil/Div.v | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 9b63fadae..d660a9935 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -116,4 +116,44 @@ Module Z. intros; apply Z.div_pos; omega. Qed. Hint Resolve div_nonneg : zarith. + + Lemma div_add_exact x y d : d <> 0 -> x mod d = 0 -> (x + y) / d = x / d + y / d. + Proof. + intros; rewrite (Z_div_exact_full_2 x d) at 1 by assumption. + rewrite Z.div_add_l' by assumption; lia. + Qed. + Hint Rewrite div_add_exact using zutil_arith : zsimplify. + + Lemma div_sub_mod_exact a b : b <> 0 -> a / b = (a - a mod b) / b. + Proof. + intro. + rewrite (Z.div_mod a b) at 2 by lia. + autorewrite with zsimplify. + reflexivity. + Qed. + + Lemma div_sub_mod_cond x y d + : d <> 0 + -> (x - y) / d + = x / d + ((x mod d - y) / d). + Proof. clear. + intro. + replace (x - y) with ((x - x mod d) + (x mod d - y)) by lia. + rewrite Z.div_add_exact by (autorewrite with pull_Zmod zsimplify; auto). + rewrite <- Z.div_sub_mod_exact by lia; lia. + 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 (autorewrite with pull_Zmod zsimplify; auto). + 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. + End Z. |