From bb4e939aae78709f243c5baf86d70fa191dff09f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 9 Apr 2018 12:47:26 -0400
Subject: Automate some proofs a bit more

---
 src/Arithmetic/BarrettReduction/Generalized.v | 50 ++++++++-------------------
 1 file changed, 15 insertions(+), 35 deletions(-)

(limited to 'src/Arithmetic')

diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v
index 1b0ebd741..54b8c7c6c 100644
--- a/src/Arithmetic/BarrettReduction/Generalized.v
+++ b/src/Arithmetic/BarrettReduction/Generalized.v
@@ -142,55 +142,40 @@ Section barrett.
 
       Lemma helper_1 : b ^ (2 * k) * ((a / n) - 1) <= m * (n * (a / n) - b ^ (k - offset)).
       Proof.
-        autorewrite with push_Zmul. ring_simplify.
-        replace (a / n * m * n) with (m * n * (a / n)) by ring.
-        assert (a/n < b ^ k) by auto using Z.div_lt_upper_bound with zarith.
-        assert (b ^ (2 * k) - m * n = b ^ (2 * k) mod n).
-        { subst m.
-          rewrite Z.mul_div_eq' by (auto using Z.lt_gt with zarith).
-          auto with zarith. }
+        pose proof (Z.mod_pos_bound (b ^ (2*k)) n).
         assert (0 < b ^ (k - offset)) by auto with zarith.
-        assert (b ^ (2*k) = b ^ (k - offset) * b ^ (k + offset)) by (rewrite <-Z.pow_add_r; auto with zarith).
-        pose proof (Z.mod_pos_bound (b ^ (2*k)) n ltac:(lia)).
-        match goal with |- ?x * (a/n) - ?c <= ?d * (a/n) - ?e =>
-                        assert ((b ^ k) * (x - d) <= c  - e); [|nia] end.
-        replace (b ^ k) with (b ^ (k - offset) * b ^ offset) by (rewrite <-Z.pow_add_r; auto with zarith).
-        nia.
+        assert (a/n < b ^ k) by auto using Z.div_lt_upper_bound with zarith.
+        assert (b ^ (2 * k) - m * n = b ^ (2 * k) mod n) by (subst m; Z.div_mod_to_quot_rem; nia).
+        autorewrite with push_Zpow in *; Z.div_mod_to_quot_rem; nia.
       Qed.
 
       Lemma helper_2 : n * (a / n) - b ^ (k - offset) < b ^ (k - offset) * (a / b ^ (k - offset)).
       Proof.
-        rewrite !Z.mul_div_eq by auto using Z.lt_gt with zarith.
-        pose proof (Z.mod_pos_bound a n ltac:(omega)).
-        pose proof (Z.mod_pos_bound a (b ^ (k - offset)) ltac:(auto with zarith)).
-        lia.
+        pose proof (Z.mod_pos_bound a n).
+        pose proof (Z.mod_pos_bound a (b ^ (k - offset))).
+        assert (0 < b ^ (k - offset)) by auto with zarith.
+        Z.div_mod_to_quot_rem; lia.
       Qed.
 
       Let epsilon := (a / n) * b ^ (k+offset) - (a / b ^ (k - offset)) * m.
 
       Lemma q_epsilon : q = (a / n) + (- epsilon) / b ^ (k + offset).
       Proof.
-        subst q. subst epsilon.
-        rewrite Z.opp_sub_distr.
-        rewrite <-Z.mul_opp_l.
-        rewrite Z.div_add_l by auto with zarith.
-        ring_simplify. f_equal; ring.
+        subst q epsilon.
+        autorewrite with push_Zpow in *; do 2 Z.div_mod_to_quot_rem; nia.
       Qed.
 
       Lemma epsilon_lower : - b ^ (k + offset) < epsilon.
       Proof.
         pose proof q_epsilon as Hq_epsilon.
         rewrite (proj2_sig q_nice) in Hq_epsilon.
-        apply Z.opp_lt_mono. rewrite Z.opp_involutive.
-        apply Z.div_le_zero; auto with zarith.
-        destruct (proj1_sig q_nice) as [ [|] [|]]; cbn [fst snd] in *; omega.
+        cut (- epsilon / b ^ (k + offset) <= 0);
+          [ Z.div_mod_to_quot_rem | break_match_hyps ]; nia.
       Qed.
 
       Lemma m_pos : 0 < m.
       Proof.
-        subst m. Z.zero_bounds.
-        split; auto with zarith.
-        transitivity (b ^ k); auto with zarith.
+        subst m. Z.zero_bounds; autorewrite with push_Zpow in *; nia.
       Qed.
 
       Lemma epsilon_bound : epsilon < b ^ (k + offset).
@@ -206,13 +191,8 @@ Section barrett.
       Proof.
         exists (0 <? epsilon).
         rewrite q_epsilon.
-        apply Z.add_cancel_l.
         pose proof epsilon_bound. pose proof epsilon_lower.
-        break_match; Z.ltb_to_lt.
-        { rewrite Z.div_opp_l_complete by auto with zarith.
-          rewrite Z.div_small, Z.mod_small by auto with zarith.
-          break_match; omega. }
-        { rewrite Z.div_small; auto with zarith. }
+        break_match; Z.ltb_to_lt; Z.div_mod_to_quot_rem; nia.
       Qed.
 
       Lemma q_bound : a / n - 1 <= q.
@@ -232,4 +212,4 @@ Section barrett.
       Qed.
     End StrongerBounds.
   End barrett_algorithm.
-End barrett.
\ No newline at end of file
+End barrett.
-- 
cgit v1.2.3