Add instances about congruence modulo

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m44.65s | Total                                           | 1m56.10s || -0m11.44s
----------------------------------------------------------------------------------
0m32.68s | Specific/GF25519                                | 0m34.42s || -0m01.74s
0m07.28s | Specific/GF1305                                 | 0m08.30s || -0m01.02s
0m03.89s | BaseSystemProofs                                | 0m04.91s || -0m01.02s
0m03.80s | ModularArithmetic/Tutorial                      | 0m05.65s || -0m01.85s
0m15.65s | ModularArithmetic/ModularBaseSystemProofs       | 0m16.40s || -0m00.74s
0m11.87s | Experiments/SpecEd25519                         | 0m12.04s || -0m00.16s
0m04.08s | ModularArithmetic/Pow2BaseProofs                | 0m04.81s || -0m00.72s
0m03.22s | ModularArithmetic/ModularBaseSystemOpt          | 0m03.37s || -0m00.14s
0m02.44s | Util/ZUtil                                      | 0m02.46s || -0m00.02s
0m02.31s | Encoding/PointEncodingPre                       | 0m02.32s || -0m00.00s
0m01.56s | ModularArithmetic/PrimeFieldTheorems            | 0m01.88s || -0m00.31s
0m01.55s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.30s || -0m00.74s
0m01.20s | BaseSystem                                      | 0m01.86s || -0m00.66s
0m01.15s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.07s || +0m00.07s
0m01.08s | ModularArithmetic/ExtendedBaseVector            | 0m01.23s || -0m00.14s
0m00.95s | ModularArithmetic/BarrettReduction/Z            | 0m01.03s || -0m00.08s
0m00.90s | Util/NumTheoryUtil                              | 0m01.29s || -0m00.39s
0m00.89s | ModularArithmetic/ModularBaseSystemField        | 0m00.93s || -0m00.04s
0m00.80s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.84s || -0m00.03s
0m00.70s | Experiments/SpecificCurve25519                  | 0m00.72s || -0m00.02s
0m00.69s | Encoding/ModularWordEncodingTheorems            | 0m00.98s || -0m00.29s
0m00.66s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.68s || -0m00.02s
0m00.63s | Testbit                                         | 0m00.71s || -0m00.07s
0m00.62s | Encoding/ModularWordEncodingPre                 | 0m00.95s || -0m00.32s
0m00.61s | ModularArithmetic/ModularBaseSystemList         | 0m00.63s || -0m00.02s
0m00.60s | Spec/ModularWordEncoding                        | 0m00.63s || -0m00.03s
0m00.59s | ModularArithmetic/ModularBaseSystem             | 0m00.57s || +0m00.02s
0m00.57s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.81s || -0m00.24s
0m00.49s | ModularArithmetic/Pre                           | 0m00.71s || -0m00.21s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.58s || -0m00.15s
0m00.40s | ModularArithmetic/Pow2Base                      | 0m00.46s || -0m00.06s
0m00.38s | Spec/ModularArithmetic                          | 0m00.56s || -0m00.18s

1 files changed, 88 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 899d1711e..045ada019 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,4 +1,6 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
+Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
+Require Import Coq.Structures.Equalities.
 Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Notations.
@@ -58,6 +60,24 @@ Hint Rewrite Z.div_small_iff using lia : zstrip_div.
     We'll put, e.g., [mul_div_eq] into it below. *)
 Create HintDb zstrip_div.
 
+Ltac comes_before ls x y :=
+  match ls with
+  | context[cons x ?xs]
+    => match xs with
+       | context[y] => idtac
+       end
+  end.
+Ltac canonicalize_comm_step mul ls comm comm3 :=
+  match goal with
+  | [ |- appcontext[mul ?x ?y] ]
+    => comes_before ls y x;
+       rewrite (comm x y)
+  | [ |- appcontext[mul ?x (mul ?y ?z)] ]
+    => comes_before ls y x;
+       rewrite (comm3 x y z)
+  end.
+Ltac canonicalize_comm mul ls comm comm3 := repeat canonicalize_comm_step mul ls comm comm3.
+
 Module Z.
   Definition pow2_mod n i := (n & (Z.ones i)).
 
@@ -68,6 +88,11 @@ Module Z.
     rewrite Z.land_ones; auto.
   Qed.
 
+  Lemma mul_comm3 x y z : x * (y * z) = y * (x * z).
+  Proof. lia. Qed.
+
+  Ltac Zcanonicalize_comm ls := canonicalize_comm Z.mul ls Z.mul_comm mul_comm3.
+
   Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
   Proof. intros; omega. Qed.
 
@@ -1078,6 +1103,69 @@ Module Z.
   Lemma two_sub_sub_inner_sub x y z : 2 * x - y - (x - z) = x - y + z.
   Proof. clear; lia. Qed.
   Hint Rewrite two_sub_sub_inner_sub : zsimplify.
+
+  Lemma f_equal_mul_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x * y) mod m = (x' * y') mod m.
+  Proof.
+    intros H0 H1; rewrite Zmult_mod, H0, H1, <- Zmult_mod; reflexivity.
+  Qed.
+  Hint Resolve f_equal_mul_mod : zarith.
+
+  Lemma f_equal_add_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x + y) mod m = (x' + y') mod m.
+  Proof.
+    intros H0 H1; rewrite Zplus_mod, H0, H1, <- Zplus_mod; reflexivity.
+  Qed.
+  Hint Resolve f_equal_add_mod : zarith.
+
+  Lemma f_equal_opp_mod x x' m : x mod m = x' mod m -> (-x) mod m = (-x') mod m.
+  Proof.
+    intro H.
+    destruct (Z_zerop (x mod m)) as [H'|H'], (Z_zerop (x' mod m)) as [H''|H''];
+      try congruence.
+    { rewrite !Z_mod_zero_opp_full by assumption; reflexivity. }
+    { rewrite Z_mod_nz_opp_full, H, <- Z_mod_nz_opp_full by assumption; reflexivity. }
+  Qed.
+  Hint Resolve f_equal_opp_mod : zarith.
+
+  Lemma f_equal_sub_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x - y) mod m = (x' - y') mod m.
+  Proof.
+    rewrite <- !Z.add_opp_r; auto with zarith.
+  Qed.
+  Hint Resolve f_equal_sub_mod : zarith.
+
+  Section equiv_modulo.
+    Context (N : Z).
+    Definition equiv_modulo x y := x mod N = y mod N.
+    Local Infix "==" := equiv_modulo.
+
+    Local Instance equiv_modulo_Reflexive : Reflexive equiv_modulo := fun _ => Logic.eq_refl.
+    Local Instance equiv_modulo_Symmetric : Symmetric equiv_modulo := fun _ _ => @Logic.eq_sym _ _ _.
+    Local Instance equiv_modulo_Transitive : Transitive equiv_modulo := fun _ _ _ => @Logic.eq_trans _ _ _ _.
+
+    Lemma mul_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.mul.
+    Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed.
+
+    Lemma add_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.add.
+    Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed.
+
+    Lemma sub_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.sub.
+    Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed.
+
+    Lemma opp_mod_Proper : Proper (equiv_modulo ==> equiv_modulo) Z.opp.
+    Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed.
+  End equiv_modulo.
+
+  Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *)
+    Existing Instance equiv_modulo_Reflexive.
+    Existing Instance equiv_modulo_Symmetric.
+    Existing Instance equiv_modulo_Transitive.
+    Existing Instance mul_mod_Proper.
+    Existing Instance add_mod_Proper.
+    Existing Instance sub_mod_Proper.
+    Existing Instance opp_mod_Proper.
+  End EquivModuloInstances.
+  Module RemoveEquivModuloInstances (dummy : Nop).
+    Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper : typeclass_instances.
+  End RemoveEquivModuloInstances.
 End Z.
 
 Module Export BoundsTactics.