From 09f49b6eb74caf65e552fcf70a23d11e6fa62133 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 2 Aug 2016 17:38:22 -0700 Subject: Add some simplification lemmas to ZUtil After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m44.13s | Total | 1m51.41s || -0m07.27s ---------------------------------------------------------------------------------- 0m32.58s | Specific/GF25519 | 0m36.11s || -0m03.53s 0m07.07s | Specific/GF1305 | 0m10.36s || -0m03.28s 0m15.34s | ModularArithmetic/ModularBaseSystemProofs | 0m15.45s || -0m00.10s 0m11.43s | Experiments/SpecEd25519 | 0m11.37s || +0m00.06s 0m04.35s | ModularArithmetic/Tutorial | 0m04.59s || -0m00.24s 0m03.95s | ModularArithmetic/Pow2BaseProofs | 0m04.05s || -0m00.09s 0m03.94s | BaseSystemProofs | 0m03.79s || +0m00.14s 0m03.16s | ModularArithmetic/ModularBaseSystemOpt | 0m03.14s || +0m00.02s 0m02.71s | Util/ZUtil | 0m02.68s || +0m00.02s 0m01.62s | ModularArithmetic/ModularArithmeticTheorems | 0m01.55s || +0m00.07s 0m01.57s | ModularArithmetic/PrimeFieldTheorems | 0m01.53s || +0m00.04s 0m01.56s | Encoding/PointEncodingPre | 0m01.62s || -0m00.06s 0m01.17s | BaseSystem | 0m01.16s || +0m00.01s 0m01.15s | ModularArithmetic/ExtendedBaseVector | 0m01.14s || +0m00.01s 0m00.98s | ModularArithmetic/BarrettReduction/Z | 0m01.07s || -0m00.09s 0m00.97s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.31s || -0m00.34s 0m00.89s | Encoding/ModularWordEncodingPre | 0m00.93s || -0m00.04s 0m00.85s | Util/NumTheoryUtil | 0m00.85s || +0m00.00s 0m00.85s | ModularArithmetic/ModularBaseSystemField | 0m00.87s || -0m00.02s 0m00.85s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.82s || +0m00.03s 0m00.80s | Spec/ModularWordEncoding | 0m00.75s || +0m00.05s 0m00.73s | Experiments/SpecificCurve25519 | 0m00.72s || +0m00.01s 0m00.71s | Encoding/ModularWordEncodingTheorems | 0m00.70s || +0m00.01s 0m00.64s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.63s || +0m00.01s 0m00.64s | Testbit | 0m00.63s || +0m00.01s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.60s || +0m00.01s 0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.58s || +0m00.03s 0m00.60s | ModularArithmetic/Pow2Base | 0m00.48s || +0m00.12s 0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.02s 0m00.49s | ModularArithmetic/Pre | 0m00.48s || +0m00.01s 0m00.39s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.46s || -0m00.07s 0m00.34s | Spec/ModularArithmetic | 0m00.42s || -0m00.07s --- src/Util/ZUtil.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 7a654d48f..1a7b54d84 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1227,6 +1227,14 @@ Module Z. Proof. intros; symmetry; apply Zminus_mod_idemp_r; assumption. Qed. Hint Rewrite sub_mod_r_push using solve [ NoZMod | lia ] : push_Zmod. + Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y. + Proof. lia. Qed. + Hint Rewrite simplify_twice_sub_sub : zsimplify. + + Lemma simplify_twice_sub_add x y : 2 * x - (x + y) = x - y. + Proof. lia. Qed. + Hint Rewrite simplify_twice_sub_add : zsimplify. + Section equiv_modulo. Context (N : Z). Definition equiv_modulo x y := x mod N = y mod N. -- cgit v1.2.3