diff options
author | Jason Gross <jagro@google.com> | 2016-07-22 16:18:37 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-22 16:22:39 -0700 |
commit | c7fd20779ca1fb4acf6e6b6cf6903f55232bf86b (patch) | |
tree | eb0fbcece930cafc9449b78ad25187b6ed34ff42 /src | |
parent | 23608c984248ac8fcf3ad126e29c69f600134a64 (diff) |
Add reverse_nondep and ring_simplify_subterms_in_all tactics
After | File Name | Before || Change
------------------------------------------------------------------------------------
2m50.48s | Total | 3m00.71s || -0m10.23s
------------------------------------------------------------------------------------
0m15.26s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m18.84s || -0m03.58s
0m48.47s | Specific/GF25519 | 0m51.03s || -0m02.56s
0m35.42s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.27s || +0m01.14s
0m09.92s | Specific/GF1305 | 0m08.66s || +0m01.25s
0m05.73s | Experiments/GenericFieldPow | 0m07.03s || -0m01.29s
0m03.67s | ModularArithmetic/Pow2BaseProofs | 0m04.78s || -0m01.11s
0m11.26s | Experiments/SpecEd25519 | 0m11.21s || +0m00.04s
0m05.81s | Algebra | 0m06.09s || -0m00.28s
0m04.54s | WeierstrassCurve/Pre | 0m05.08s || -0m00.54s
0m03.62s | ModularArithmetic/Tutorial | 0m04.38s || -0m00.75s
0m03.34s | CompleteEdwardsCurve/Pre | 0m03.56s || -0m00.22s
0m02.83s | ModularArithmetic/ModularBaseSystemOpt | 0m03.37s || -0m00.54s
0m01.76s | Experiments/EdDSARefinement | 0m01.81s || -0m00.05s
0m01.54s | ModularArithmetic/PrimeFieldTheorems | 0m01.67s || -0m00.12s
0m01.52s | ModularArithmetic/ModularArithmeticTheorems | 0m01.62s || -0m00.10s
0m01.47s | Encoding/PointEncodingPre | 0m01.63s || -0m00.15s
0m01.21s | ModularArithmetic/ExtendedBaseVector | 0m01.33s || -0m00.12s
0m00.99s | Experiments/SpecificCurve25519 | 0m00.95s || +0m00.04s
0m00.98s | ModularArithmetic/ModularBaseSystemProofs | 0m01.08s || -0m00.10s
0m00.90s | ModularArithmetic/BarrettReduction/Z | 0m00.96s || -0m00.05s
0m00.87s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.88s || -0m00.01s
0m00.86s | ModularArithmetic/ModularBaseSystemField | 0m00.99s || -0m00.13s
0m00.81s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.94s || -0m00.12s
0m00.71s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.69s || +0m00.02s
0m00.67s | Util/IterAssocOp | 0m00.74s || -0m00.06s
0m00.65s | Encoding/ModularWordEncodingTheorems | 0m00.68s || -0m00.03s
0m00.64s | Testbit | 0m00.63s || +0m00.01s
0m00.61s | Util/AdditionChainExponentiation | 0m00.68s || -0m00.07s
0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.72s || -0m00.10s
0m00.61s | Encoding/ModularWordEncodingPre | 0m00.82s || -0m00.20s
0m00.60s | Spec/EdDSA | 0m00.60s || +0m00.00s
0m00.59s | ModularArithmetic/ModularBaseSystemList | 0m00.87s || -0m00.28s
0m00.57s | Spec/ModularWordEncoding | 0m00.62s || -0m00.05s
0m00.57s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.61s || -0m00.04s
0m00.43s | Spec/WeierstrassCurve | 0m00.43s || +0m00.00s
0m00.40s | Spec/CompleteEdwardsCurve | 0m00.44s || -0m00.03s
0m00.04s | Util/Tactics | 0m00.03s || +0m00.01s
Diffstat (limited to 'src')
-rw-r--r-- | src/Algebra.v | 3 | ||||
-rw-r--r-- | src/Util/Tactics.v | 14 |
2 files changed, 17 insertions, 0 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index f71807fff..153871d4c 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1304,6 +1304,9 @@ Ltac only_two_square_roots := Require Import Coq.setoid_ring.Ring_tac. 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. + 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. diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 5ff9d203c..aa8093308 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -308,3 +308,17 @@ Ltac tac_on_subterms tac := | [ |- context[?t] ] => progress tac t end. + +(** Like [Coq.Program.Tactics.revert_last], but only for non-dependent hypotheses *) +Ltac revert_last_nondep := + match goal with + | [ H : _ |- _ ] + => lazymatch goal with + | [ H' : appcontext[H] |- _ ] => fail + | [ |- appcontext[H] ] => fail + | _ => idtac + end; + revert H + end. + +Ltac reverse_nondep := repeat revert_last_nondep. |