From 04825173022abc6e38d8e95651b9194460d6956a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 29 Jul 2016 14:48:26 -0700 Subject: 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 --- src/Util/ZUtil.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'src') 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. -- cgit v1.2.3