Add equiv_modulo rewrite instances

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m48.87s | Total                                           | 1m54.96s || -0m06.09s
----------------------------------------------------------------------------------
0m04.05s | ModularArithmetic/Tutorial                      | 0m05.62s || -0m01.57s
0m33.97s | Specific/GF25519                                | 0m33.49s || +0m00.47s
0m16.98s | ModularArithmetic/ModularBaseSystemProofs       | 0m16.59s || +0m00.39s
0m12.24s | Experiments/SpecEd25519                         | 0m12.42s || -0m00.17s
0m07.11s | Specific/GF1305                                 | 0m07.51s || -0m00.39s
0m04.45s | ModularArithmetic/Pow2BaseProofs                | 0m05.43s || -0m00.97s
0m03.94s | BaseSystemProofs                                | 0m04.03s || -0m00.09s
0m03.22s | ModularArithmetic/ModularBaseSystemOpt          | 0m03.25s || -0m00.02s
0m02.61s | Util/ZUtil                                      | 0m02.61s || +0m00.00s
0m01.88s | Encoding/PointEncodingPre                       | 0m02.34s || -0m00.46s
0m01.65s | ModularArithmetic/PrimeFieldTheorems            | 0m02.02s || -0m00.37s
0m01.65s | ModularArithmetic/ModularArithmeticTheorems     | 0m01.76s || -0m00.11s
0m01.19s | BaseSystem                                      | 0m01.45s || -0m00.26s
0m01.10s | ModularArithmetic/ExtendedBaseVector            | 0m01.41s || -0m00.30s
0m01.04s | Encoding/ModularWordEncodingTheorems            | 0m01.01s || +0m00.03s
0m01.01s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.41s || -0m00.39s
0m00.95s | ModularArithmetic/BarrettReduction/Z            | 0m01.02s || -0m00.07s
0m00.95s | Encoding/ModularWordEncodingPre                 | 0m00.71s || +0m00.24s
0m00.89s | ModularArithmetic/ModularBaseSystemField        | 0m00.92s || -0m00.03s
0m00.85s | Util/NumTheoryUtil                              | 0m00.92s || -0m00.07s
0m00.83s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.89s || -0m00.06s
0m00.75s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.88s || -0m00.13s
0m00.74s | Experiments/SpecificCurve25519                  | 0m00.75s || -0m00.01s
0m00.62s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.96s || -0m00.34s
0m00.61s | ModularArithmetic/ModularBaseSystemList         | 0m00.65s || -0m00.04s
0m00.60s | Spec/ModularWordEncoding                        | 0m00.89s || -0m00.29s
0m00.60s | Testbit                                         | 0m01.00s || -0m00.40s
0m00.58s | ModularArithmetic/ModularBaseSystem             | 0m00.64s || -0m00.06s
0m00.51s | Spec/ModularArithmetic                          | 0m00.46s || +0m00.04s
0m00.48s | ModularArithmetic/Pre                           | 0m00.68s || -0m00.20s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.62s || -0m00.20s
0m00.41s | ModularArithmetic/Pow2Base                      | 0m00.63s || -0m00.22s

1 files changed, 11 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 7b7daef67..670227ba8 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1202,6 +1202,14 @@ Module Z.
 
     Lemma opp_mod_Proper : Proper (equiv_modulo ==> equiv_modulo) Z.opp.
     Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed.
+
+    Lemma modulo_equiv_modulo_Proper
+      : Proper (equiv_modulo ==> (fun x y => x = N /\ N = y) ==> Logic.eq) Z.modulo.
+    Proof.
+      repeat intro; hnf in *; intuition congruence.
+    Qed.
+    Lemma eq_to_ProperProxy : ProperProxy (fun x y : Z => x = N /\ N = y) N.
+    Proof. split; reflexivity. Qed.
   End equiv_modulo.
 
   Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *)
@@ -1212,9 +1220,11 @@ Module Z.
     Existing Instance add_mod_Proper.
     Existing Instance sub_mod_Proper.
     Existing Instance opp_mod_Proper.
+    Existing Instance modulo_equiv_modulo_Proper.
+    Existing Instance eq_to_ProperProxy.
   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.
+    Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances.
   End RemoveEquivModuloInstances.
 End Z.