More zutil lemmas

After     | File Name                                                    | Before    || Change
-------------------------------------------------------------------------------------------------
10m45.67s | Total                                                        | 10m43.13s || +0m02.53s
-------------------------------------------------------------------------------------------------
2m16.12s  | Specific/IntegrationTestLadderstep                           | 2m14.60s  || +0m01.52s
1m38.08s  | Spec/Test/X25519                                             | 1m39.94s  || -0m01.85s
0m59.86s  | Specific/IntegrationTestLadderstep130                        | 0m58.23s  || +0m01.63s
0m16.71s  | Util/ZUtil                                                   | 0m15.52s  || +0m01.19s
0m48.39s  | Compilers/Z/ArithmeticSimplifierWf                           | 0m48.40s  || -0m00.00s
0m39.53s  | Spec/Ed25519                                                 | 0m39.40s  || +0m00.13s
0m19.63s  | Compilers/Named/MapCastWf                                    | 0m19.67s  || -0m00.04s
0m17.49s  | Primitives/EdDSARepChange                                    | 0m17.66s  || -0m00.17s
0m12.25s  | Specific/IntegrationTestMul                                  | 0m12.10s  || +0m00.15s
0m10.86s  | Compilers/Z/ArithmeticSimplifierInterp                       | 0m11.03s  || -0m00.16s
0m10.59s  | Specific/IntegrationTestSquare                               | 0m10.59s  || +0m00.00s
0m09.94s  | Specific/IntegrationTestSub                                  | 0m10.08s  || -0m00.14s
0m09.30s  | Compilers/Named/MapCastInterp                                | 0m09.30s  || +0m00.00s
0m09.20s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy          | 0m09.22s  || -0m00.02s
0m08.62s  | Arithmetic/MontgomeryReduction/Proofs                        | 0m08.62s  || +0m00.00s
0m08.51s  | LegacyArithmetic/ArchitectureToZLikeProofs                   | 0m08.70s  || -0m00.18s
0m08.04s  | LegacyArithmetic/Double/Proofs/Multiply                      | 0m08.07s  || -0m00.03s
0m07.75s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m07.84s  || -0m00.08s
0m07.67s  | Specific/ArithmeticSynthesisTest                             | 0m07.62s  || +0m00.04s
0m06.81s  | Arithmetic/Core                                              | 0m06.81s  || +0m00.00s
0m06.60s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate           | 0m06.58s  || +0m00.01s
0m06.41s  | Util/FixedWordSizesEquality                                  | 0m06.42s  || -0m00.00s
0m05.34s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub             | 0m05.40s  || -0m00.06s
0m05.30s  | LegacyArithmetic/Pow2BaseProofs                              | 0m05.21s  || +0m00.08s
0m05.01s  | Specific/ArithmeticSynthesisTest130                          | 0m05.00s  || +0m00.00s
0m03.84s  | Arithmetic/BarrettReduction/HAC                              | 0m03.69s  || +0m00.14s
0m03.54s  | Arithmetic/Saturated                                         | 0m03.42s  || +0m00.12s
0m03.41s  | LegacyArithmetic/InterfaceProofs                             | 0m03.33s  || +0m00.08s
0m03.12s  | Specific/FancyMachine256/Montgomery                          | 0m03.13s  || -0m00.00s
0m02.99s  | Arithmetic/BarrettReduction/Generalized                      | 0m03.00s  || -0m00.00s
0m02.90s  | Specific/FancyMachine256/Barrett                             | 0m02.89s  || +0m00.00s
0m02.89s  | LegacyArithmetic/ZBoundedZ                                   | 0m03.01s  || -0m00.11s
0m02.83s  | Arithmetic/ModularArithmeticTheorems                         | 0m02.84s  || -0m00.00s
0m02.56s  | LegacyArithmetic/Double/Proofs/ShiftRight                    | 0m02.53s  || +0m00.03s
0m02.48s  | LegacyArithmetic/Double/Proofs/ShiftLeft                     | 0m02.50s  || -0m00.02s
0m02.48s  | LegacyArithmetic/Double/Proofs/Decode                        | 0m02.43s  || +0m00.04s
0m02.31s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast             | 0m02.36s  || -0m00.04s
0m02.30s  | Compilers/Z/Bounds/Relax                                     | 0m02.28s  || +0m00.02s
0m02.13s  | LegacyArithmetic/BarretReduction                             | 0m02.09s  || +0m00.04s
0m02.00s  | Util/WordUtil                                                | 0m02.00s  || +0m00.00s
0m01.92s  | Specific/FancyMachine256/Core                                | 0m01.82s  || +0m00.09s
0m01.52s  | Arithmetic/PrimeFieldTheorems                                | 0m01.48s  || +0m00.04s
0m01.51s  | LegacyArithmetic/MontgomeryReduction                         | 0m01.51s  || +0m00.00s
0m01.48s  | Arithmetic/BarrettReduction/Wikipedia                        | 0m01.52s  || -0m00.04s
0m01.25s  | Compilers/Z/Syntax/Equality                                  | 0m01.22s  || +0m00.03s
0m01.24s  | Compilers/Z/Bounds/Pipeline/Definition                       | 0m01.24s  || +0m00.00s
0m00.98s  | Util/NumTheoryUtil                                           | 0m00.94s  || +0m00.04s
0m00.91s  | LegacyArithmetic/Double/Proofs/LoadImmediate                 | 0m00.82s  || +0m00.09s
0m00.89s  | Arithmetic/Karatsuba                                         | 0m00.86s  || +0m00.03s
0m00.84s  | LegacyArithmetic/Double/Proofs/BitwiseOr                     | 0m00.80s  || +0m00.03s
0m00.79s  | LegacyArithmetic/BaseSystemProofs                            | 0m00.84s  || -0m00.04s
0m00.74s  | Compilers/MapCastByDeBruijnInterp                            | 0m00.67s  || +0m00.06s
0m00.71s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                | 0m00.70s  || +0m00.01s
0m00.68s  | Util/ZUtil/Stabilization                                     | 0m00.66s  || +0m00.02s
0m00.68s  | Compilers/Z/Syntax/Util                                      | 0m00.70s  || -0m00.01s
0m00.67s  | Util/IterAssocOp                                             | 0m00.71s  || -0m00.03s
0m00.60s  | LegacyArithmetic/Interface                                   | 0m00.64s  || -0m00.04s
0m00.56s  | Compilers/Z/CommonSubexpressionElimination                   | 0m00.51s  || +0m00.05s
0m00.56s  | Compilers/MapCastByDeBruijnWf                                | 0m00.53s  || +0m00.03s
0m00.54s  | LegacyArithmetic/Double/Proofs/SelectConditional             | 0m00.60s  || -0m00.05s
0m00.50s  | Arithmetic/ModularArithmeticPre                              | 0m00.46s  || +0m00.03s
0m00.50s  | Compilers/Z/Reify                                            | 0m00.46s  || +0m00.03s
0m00.49s  | Compilers/Z/FoldTypes                                        | 0m00.31s  || +0m00.18s
0m00.48s  | Util/NUtil                                                   | 0m00.52s  || -0m00.04s
0m00.47s  | LegacyArithmetic/ZBounded                                    | 0m00.47s  || +0m00.00s
0m00.46s  | LegacyArithmetic/Pow2Base                                    | 0m00.40s  || +0m00.06s
0m00.46s  | LegacyArithmetic/Double/Core                                 | 0m00.44s  || +0m00.02s
0m00.46s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                   | 0m00.47s  || -0m00.00s
0m00.45s  | Compilers/Z/Bounds/Pipeline                                  | 0m00.45s  || +0m00.00s
0m00.45s  | Compilers/Z/Bounds/Pipeline/Glue                             | 0m00.49s  || -0m00.03s
0m00.45s  | LegacyArithmetic/ArchitectureToZLike                         | 0m00.42s  || +0m00.03s
0m00.44s  | Spec/EdDSA                                                   | 0m00.49s  || -0m00.04s
0m00.42s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics              | 0m00.42s  || +0m00.00s
0m00.42s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic          | 0m00.42s  || +0m00.00s
0m00.40s  | LegacyArithmetic/BaseSystem                                  | 0m00.48s  || -0m00.07s
0m00.39s  | Compilers/Z/CommonSubexpressionEliminationWf                 | 0m00.38s  || +0m00.01s
0m00.39s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                       | 0m00.44s  || -0m00.04s
0m00.38s  | Compilers/Z/Bounds/MapCastByDeBruijn                         | 0m00.40s  || -0m00.02s
0m00.37s  | Compilers/Z/MapCastByDeBruijnInterp                          | 0m00.36s  || +0m00.01s
0m00.37s  | Arithmetic/MontgomeryReduction/Definition                    | 0m00.36s  || +0m00.01s
0m00.37s  | Compilers/Z/MapCastByDeBruijnWf                              | 0m00.40s  || -0m00.03s
0m00.35s  | Spec/ModularArithmetic                                       | 0m00.36s  || -0m00.01s
0m00.35s  | Compilers/Z/InlineWf                                         | 0m00.39s  || -0m00.04s
0m00.34s  | Compilers/Z/Inline                                           | 0m00.34s  || +0m00.00s
0m00.33s  | Compilers/Z/InlineInterp                                     | 0m00.34s  || -0m00.01s
0m00.32s  | Compilers/Z/CommonSubexpressionEliminationInterp             | 0m00.39s  || -0m00.07s

1 files changed, 44 insertions, 2 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 87dec1cf9..a7d511136 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -55,12 +55,13 @@ Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.
 Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2.
 Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag : zsimplify_fast.
 
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag : zsimplify.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 : zsimplify.
 Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full Z.mod_1_l using zutil_arith : zsimplify.
 Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify.
 Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify.
 Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify.
-Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 : zsimplify_const.
+Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 : zsimplify_const.
+
 Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const.
 
 (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *)
@@ -2904,6 +2905,47 @@ Module Z.
     rewrite Z.div_small; lia.
   Qed.
 
+  Lemma quot_small_abs a b : 0 <= Z.abs a < Z.abs b -> Z.quot a b = 0.
+  Proof.
+    intros; rewrite Z.quot_small_iff by lia; lia.
+  Qed.
+
+  Lemma quot_add_sub_sgn_small a b : b <> 0 -> Z.sgn a = Z.sgn b -> Z.quot (a + b - Z.sgn b) b = Z.quot (a - Z.sgn b) b + 1.
+  Proof.
+    destruct (Z_zerop a), (Z_zerop b), (Z_lt_le_dec a 0), (Z_lt_le_dec b 0), (Z_lt_le_dec 1 (Z.abs a));
+      subst;
+      try lia;
+      rewrite !Z.quot_div_full;
+      try rewrite (Z.sgn_neg a) by omega;
+      try rewrite (Z.sgn_neg b) by omega;
+      repeat first [ reflexivity
+                   | rewrite Z.sgn_neg by lia
+                   | rewrite Z.sgn_pos by lia
+                   | rewrite Z.abs_eq by lia
+                   | rewrite Z.abs_neq by lia
+                   | rewrite !Z.mul_opp_l
+                   | rewrite Z.abs_opp in *
+                   | rewrite Z.abs_eq in * by omega
+                   | match goal with
+                     | [ |- context[-1 * ?x] ]
+                       => replace (-1 * x) with (-x) by omega
+                     | [ |- context[?x * -1] ]
+                       => replace (x * -1) with (-x) by omega
+                     | [ |- context[-?x - ?y] ]
+                       => replace (-x - y) with (-(x + y)) by omega
+                     | [ |- context[-?x + - ?y] ]
+                       => replace (-x + - y) with (-(x + y)) by omega
+                     | [ |- context[(?a + ?b + ?c) / ?b] ]
+                       => replace (a + b + c) with (((a + c) + b * 1)) by lia; rewrite Z.div_add' by omega
+                     | [ |- context[(?a + ?b - ?c) / ?b] ]
+                       => replace (a + b - c) with (((a - c) + b * 1)) by lia; rewrite Z.div_add' by omega
+                     end
+                   | progress intros
+                   | progress Z.replace_all_neg_with_pos
+                   | progress autorewrite with zsimplify ].
+  Qed.
+
+
   (* Naming Convention: [X] for thing being divided by, [p] for plus,
      [m] for minus, [d] for div, and [_] to separate parentheses and
      multiplication. *)