diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-10 17:32:30 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-10 17:32:30 -0400 |
commit | 3968273d002716ba3a159e3c36b7661e4449ec40 (patch) | |
tree | 4f2a8e971cf4a64e51c9ee65c936b46d638317a3 /src/Util/ZUtil/Modulo.v | |
parent | 3fa4f686d5425782a4cbc0aaca4f2bcbf2a5c060 (diff) |
Add mod_pull_div{,_full}
Diffstat (limited to 'src/Util/ZUtil/Modulo.v')
-rw-r--r-- | src/Util/ZUtil/Modulo.v | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index f4405bef3..d402055dd 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -149,6 +149,79 @@ Module Z. Qed. Hint Rewrite mod_div_eq0 using zutil_arith : zsimplify. + Local Lemma mod_pull_div_helper a b c X + (HX : forall a b c d e f g, + X a b c d e f g = if a =? 0 then c else 0) + : 0 <> b + -> 0 <> c + -> (a / b) mod c + = (a mod (c * b)) / b + + if c <? 0 then - X ((a / b) mod c) (a mod (c * b)) ((a mod (c * b)) / b) a b c (a / b) else 0. + Proof. + intros; break_match; Z.ltb_to_lt; rewrite ?Z.sub_0_r, ?Z.add_0_r; + assert (0 <> c * b) by nia; Z.div_mod_to_quot_rem; subst; + destruct_head'_or; destruct_head'_and; + try assert (b < 0) by omega; + try assert (c < 0) by omega; + Z.replace_all_neg_with_pos; + try match goal with + | [ H : ?c * ?b * ?q1 + ?r1 = ?b * (?c * ?q2 + _) + _ |- _ ] + => assert (q1 = q2) by nia; progress subst + end; + rewrite ?HX; clear HX X; + try nia; + repeat match goal with + | [ |- - ?x = ?y ] => is_var y; assert (y <= 0) by nia; Z.replace_all_neg_with_pos + | [ |- - ?x = ?y + -_ ] => is_var y; assert (y <= 0) by nia; Z.replace_all_neg_with_pos + | [ H : -?x + (-?y + ?z) = -?w + ?v |- _ ] + => assert (x + (y + -z) = w + -v) by omega; clear H + | [ H : ?c * ?b * ?q1 + (?b * ?q2 + ?r) = ?b * (?c * ?q1' + ?q2') + ?r' |- _ ] + => assert (c * q1 + q2 = c * q1' + q2') by nia; + assert (r = r') by nia; + clear H + | [ H : -?x < -?y + ?z |- _ ] => assert (y + -z < x) by omega; clear H + | [ H : -?x + ?y <= 0 |- _ ] => assert (0 <= x + -y) by omega; clear H + | _ => progress Z.clean_neg + | _ => progress subst + end. + all:match goal with + | [ H : ?c * ?q + ?r = ?c * ?q' + ?r' |- _ ] + => first [ constr_eq q q'; assert (r = r') by nia; clear H + | assert (q = q') by nia; assert (r = r') by nia; clear H + | lazymatch goal with + | [ H' : r' < c |- _ ] + => destruct (Z_dec' r c) as [[?|?]|?] + | [ H' : r < c |- _ ] + => destruct (Z_dec' r' c) as [[?|?]|?] + end; + subst; + [ assert (q = q') by nia; assert (r = r') by nia; clear H + | nia + | first [ assert (1 + q = q') by nia | assert (q = 1 + q') by nia ]; + first [ assert (r' = 0) by nia | assert (r = 0) by nia ] ] ] + end. + all:try omega. + all:break_match; Z.ltb_to_lt; omega. + Qed. + + Lemma mod_pull_div_full a b c + : (a / b) mod c + = if ((c <? 0) && ((a / b) mod c =? 0))%bool + then 0 + else (a mod (c * b)) / b. + Proof. + destruct (Z_zerop b), (Z_zerop c); subst; + autorewrite with zsimplify; try reflexivity. + { break_match; Z.ltb_to_lt; omega. } + { erewrite mod_pull_div_helper at 1 by (omega || reflexivity); cbv beta. + destruct (c <? 0) eqn:?; simpl; [ | omega ]. + break_innermost_match; omega. } + Qed. + + Lemma mod_pull_div a b c + : 0 <= c -> (a / b) mod c = a mod (c * b) / b. + Proof. rewrite mod_pull_div_full; destruct (c <? 0) eqn:?; Z.ltb_to_lt; simpl; omega. Qed. + Lemma mod_pow_full p q n : (p^q) mod n = ((p mod n)^q) mod n. Proof. destruct (Z_dec' n 0) as [ [H|H] | H]; subst; |