From 279781a50da8f1ae58faba1e81055310ca484be0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Mar 2017 17:21:44 -0400 Subject: Make Z.rewrite_mod_small a bit more powerful Now it can handle things like ((x mod 4) mod 2) when we have (x mod 4 < 2) as a hypothesis. --- src/Util/ZUtil.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c63a9028d..64604022a 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2532,6 +2532,28 @@ Module Z. Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step; intros. + Lemma mod_mod_small a n m + (Hnm : (m mod n = 0)%Z) + (Hnm_le : (0 < n <= m)%Z) + (H : (a mod m < n)%Z) + : ((a mod n) mod m = a mod m)%Z. + Proof. + assert ((a mod n) < m)%Z + by (eapply Z.lt_le_trans; [ apply Z.mod_pos_bound | ]; omega). + rewrite (Z.mod_small _ m) by auto with zarith. + apply Z.mod_divide in Hnm; [ | omega ]. + destruct Hnm as [x ?]; subst. + repeat match goal with + | [ H : context[(_ mod _)%Z] |- _ ] + => revert H + end. + Z.div_mod_to_quot_rem. + lazymatch goal with + | [ H : a = (?x * ?n * ?q) + _, H' : a = (?n * ?q') + _ |- _ ] + => assert (q' = x * q) by nia; subst q'; nia + end. + Qed. + (** [rewrite_mod_small] is a better version of [rewrite Z.mod_small by rewrite_mod_small_solver]; it backtracks across occurences that the solver fails to solve the side-conditions on. *) @@ -2541,6 +2563,8 @@ Module Z. repeat match goal with | [ |- context[?x mod ?y] ] => rewrite (Z.mod_small x y) by rewrite_mod_small_solver + | [ |- context[(?a mod ?n) mod ?m] ] + => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver end. Local Ltac simplify_div_tac := -- cgit v1.2.3