diff options
author | Jason Gross <jagro@google.com> | 2016-08-16 18:51:16 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-08-16 18:58:03 -0700 |
commit | 0adb3274ec03fac61696a0e16027f23dfb1f88db (patch) | |
tree | 0d9cd21320b2ee0da8e3a39bb5219e9ae0e587c3 /src | |
parent | 42a122726ea5a1d42009718e965a9860fab83463 (diff) |
Add natutil
After | File Name | Before || Change
------------------------------------------------------------------------------------
4m05.87s | Total | 3m55.03s || +0m10.84s
------------------------------------------------------------------------------------
0m29.03s | ModularArithmetic/Pow2BaseProofs | 0m22.86s || +0m06.17s
0m42.14s | CompleteEdwardsCurve/ExtendedCoordinates | 0m37.78s || +0m04.35s
0m33.70s | Specific/GF25519 | 0m36.48s || -0m02.77s
0m18.10s | ModularArithmetic/ModularBaseSystemProofs | 0m16.95s || +0m01.15s
0m09.83s | ModularArithmetic/Montgomery/ZProofs | 0m08.72s || +0m01.10s
0m08.38s | Specific/GF1305 | 0m06.89s || +0m01.49s
0m04.00s | ModularArithmetic/ModularArithmeticTheorems | 0m02.62s || +0m01.37s
0m03.61s | ModularArithmetic/Tutorial | 0m05.40s || -0m01.79s
0m16.27s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.14s || +0m00.12s
0m13.68s | Experiments/SpecEd25519 | 0m13.66s || +0m00.01s
0m10.18s | Util/ZUtil | 0m09.70s || +0m00.48s
0m08.91s | Testbit | 0m09.14s || -0m00.23s
0m03.99s | BaseSystemProofs | 0m03.85s || +0m00.14s
0m03.96s | Util/ListUtil | 0m04.19s || -0m00.23s
0m03.60s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.59s || +0m00.01s
0m03.37s | Experiments/SpecificCurve25519 | 0m03.36s || +0m00.01s
0m02.90s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.90s || +0m00.00s
0m02.51s | Experiments/EdDSARefinement | 0m01.78s || +0m00.72s
0m02.28s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.35s || -0m00.07s
0m02.25s | ModularArithmetic/ModularBaseSystemOpt | 0m02.27s || -0m00.02s
0m01.58s | Util/Tuple | 0m01.63s || -0m00.04s
0m01.53s | Encoding/PointEncodingPre | 0m02.33s || -0m00.80s
0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m01.54s || -0m00.07s
0m01.27s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.93s || +0m00.34s
0m01.19s | Util/NatUtil | 0m01.10s || +0m00.08s
0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.18s || +0m00.01s
0m01.18s | BaseSystem | 0m01.20s || -0m00.02s
0m01.17s | ModularArithmetic/PrimeFieldTheorems | 0m01.04s || +0m00.12s
0m00.97s | Util/NumTheoryUtil | 0m00.86s || +0m00.10s
0m00.88s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.94s || -0m00.05s
0m00.87s | ModularArithmetic/ModularBaseSystemField | 0m00.92s || -0m00.05s
0m00.84s | ModularArithmetic/Montgomery/ZBounded | 0m00.88s || -0m00.04s
0m00.78s | Spec/ModularWordEncoding | 0m00.68s || +0m00.09s
0m00.68s | Encoding/ModularWordEncodingTheorems | 0m00.75s || -0m00.06s
0m00.66s | Encoding/ModularWordEncodingPre | 0m00.79s || -0m00.13s
0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.78s || -0m00.13s
0m00.65s | Util/AdditionChainExponentiation | 0m00.67s || -0m00.02s
0m00.65s | Spec/EdDSA | 0m00.92s || -0m00.27s
0m00.63s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.64s || -0m00.01s
0m00.62s | ModularArithmetic/ModularBaseSystemList | 0m00.64s || -0m00.02s
0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.60s || +0m00.01s
0m00.52s | ModularArithmetic/Pre | 0m00.49s || +0m00.03s
0m00.50s | Util/WordUtil | 0m00.62s || -0m00.12s
0m00.45s | ModularArithmetic/Pow2Base | 0m00.47s || -0m00.01s
0m00.44s | ModularArithmetic/ZBounded | 0m00.44s || +0m00.00s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.39s || +0m00.02s
0m00.40s | ModularArithmetic/Montgomery/Z | 0m00.41s || -0m00.00s
0m00.38s | Spec/ModularArithmetic | 0m00.56s || -0m00.18s
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/NatUtil.v | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 5c65148c0..344eb40c9 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -10,7 +10,7 @@ Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify. -Hint Rewrite sub_diag add_0_l add_0_r sub_0_r : natsimplify. +Hint Rewrite sub_diag add_0_l add_0_r sub_0_r sub_succ : natsimplify. Local Open Scope nat_scope. @@ -66,7 +66,7 @@ Proof. reflexivity. Qed. -Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. +Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. Proof. intros; apply Nat.mod_small. destruct m; try omega; rewrite Nat.pred_succ; auto. @@ -291,3 +291,15 @@ Proof. apply f_equal, le_unique. Qed. Hint Rewrite le_dec_pred_plus_same : natsimplify. + +Lemma minus_S_diag x : (S x - x = 1)%nat. +Proof. omega. Qed. +Hint Rewrite minus_S_diag : natsimplify. + +Lemma min_idempotent_S_l x : min (S x) x = x. +Proof. omega *. Qed. +Hint Rewrite min_idempotent_S_l : natsimplify. + +Lemma min_idempotent_S_r x : min x (S x) = x. +Proof. omega *. Qed. +Hint Rewrite min_idempotent_S_r : natsimplify. |