From 1ccd4575a0bc82064e38d4b20b2cd3088e2f4205 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Jul 2016 16:47:44 -0700 Subject: Add databases for ring_simplify After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m39.49s | Total | 2m36.24s || +0m03.25s ------------------------------------------------------------------------------------ 0m48.49s | Specific/GF25519 | 0m48.53s || -0m00.03s 0m34.52s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.24s || +0m00.28s 0m15.71s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.24s || +0m00.47s 0m11.41s | Experiments/SpecEd25519 | 0m11.34s || +0m00.07s 0m08.23s | Specific/GF1305 | 0m08.30s || -0m00.07s 0m05.64s | Algebra | 0m05.55s || +0m00.08s 0m05.03s | WeierstrassCurve/Pre | 0m04.51s || +0m00.52s 0m04.23s | ModularArithmetic/Tutorial | 0m03.63s || +0m00.60s 0m03.33s | CompleteEdwardsCurve/Pre | 0m03.34s || -0m00.00s 0m02.87s | ModularArithmetic/ModularBaseSystemOpt | 0m02.80s || +0m00.07s 0m01.80s | Experiments/EdDSARefinement | 0m01.77s || +0m00.03s 0m01.54s | ModularArithmetic/PrimeFieldTheorems | 0m01.55s || -0m00.01s 0m01.52s | Encoding/PointEncodingPre | 0m01.54s || -0m00.02s 0m01.51s | ModularArithmetic/ModularArithmeticTheorems | 0m01.51s || +0m00.00s 0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.18s || +0m00.01s 0m01.16s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.80s || +0m00.35s 0m01.03s | ModularArithmetic/ModularBaseSystemProofs | 0m00.96s || +0m00.07s 0m00.95s | Experiments/SpecificCurve25519 | 0m00.95s || +0m00.00s 0m00.92s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.85s || +0m00.07s 0m00.91s | ModularArithmetic/ModularBaseSystemField | 0m00.86s || +0m00.05s 0m00.76s | Encoding/ModularWordEncodingPre | 0m00.60s || +0m00.16s 0m00.69s | Util/IterAssocOp | 0m00.67s || +0m00.01s 0m00.69s | ModularArithmetic/ModularBaseSystemList | 0m00.57s || +0m00.12s 0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.63s || +0m00.05s 0m00.68s | Spec/EdDSA | 0m00.61s || +0m00.07s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.64s || +0m00.03s 0m00.66s | Spec/ModularWordEncoding | 0m00.56s || +0m00.09s 0m00.62s | Util/AdditionChainExponentiation | 0m00.59s || +0m00.03s 0m00.58s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.01s 0m00.55s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.54s || +0m00.01s 0m00.51s | Spec/WeierstrassCurve | 0m00.43s || +0m00.08s 0m00.41s | Spec/CompleteEdwardsCurve | 0m00.38s || +0m00.02s --- src/Algebra.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Algebra.v b/src/Algebra.v index 153871d4c..f4afcb935 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1307,6 +1307,14 @@ Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t). Ltac ring_simplify_subterms_in_all := reverse_nondep; ring_simplify_subterms; intros. +Create HintDb ring_simplify discriminated. +Create HintDb ring_simplify_subterms discriminated. +Create HintDb ring_simplify_subterms_in_all discriminated. +Hint Extern 1 => progress ring_simplify : ring_simplify. +Hint Extern 1 => progress ring_simplify_subterms : ring_simplify_subterms. +Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all. + + Section Example. Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. -- cgit v1.2.3