More fine-grained tactic imports

Most files no longer import Crypto.Util.Tactics.

We remove an unused lemma depending on classical axioms; closes #143.

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
28m38.18s | Total                                                                  | 29m04.51s || -0m26.32s
-----------------------------------------------------------------------------------------------------------
0m41.70s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m32.66s  || +0m09.04s
1m39.88s  | MontgomeryX                                                            | 1m46.07s  || -0m06.18s
1m56.52s  | WeierstrassCurve/Projective                                            | 2m00.76s  || -0m04.23s
10m36.85s | WeierstrassCurve/WeierstrassCurveTheorems                              | 10m40.14s || -0m03.28s
0m21.35s  | ModularArithmetic/Pow2BaseProofs                                       | 0m22.54s  || -0m01.18s
0m20.24s  | Reflection/Named/MapCastWf                                             | 0m21.41s  || -0m01.17s
1m30.28s  | Test/Curve25519SpecTestVectors                                         | 1m31.19s  || -0m00.90s
0m49.53s  | Specific/IntegrationTest                                               | 0m50.01s  || -0m00.47s
0m42.19s  | MontgomeryCurveTheorems                                                | 0m42.18s  || +0m00.00s
0m41.08s  | ModularArithmetic/Conversion                                           | 0m41.84s  || -0m00.76s
0m36.62s  | Spec/Ed25519                                                           | 0m37.13s  || -0m00.51s
0m23.64s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m24.44s  || -0m00.80s
0m19.94s  | Specific/GF25519                                                       | 0m20.12s  || -0m00.17s
0m19.59s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 0m19.83s  || -0m00.23s
0m19.14s  | Reflection/Z/Bounds/InterpretationLemmas                               | 0m19.90s  || -0m00.75s
0m18.65s  | EdDSARepChange                                                         | 0m18.74s  || -0m00.08s
0m16.24s  | Reflection/Z/ArithmeticSimplifierWf                                    | 0m17.11s  || -0m00.87s
0m15.03s  | Util/ZUtil                                                             | 0m15.93s  || -0m00.90s
0m14.74s  | Reflection/Named/ContextProperties/NameUtil                            | 0m15.11s  || -0m00.36s
0m14.62s  | Reflection/Named/ContextProperties/SmartMap                            | 0m14.93s  || -0m00.31s
0m12.96s  | Specific/NewBaseSystemTest                                             | 0m13.24s  || -0m00.27s
0m11.84s  | Algebra/Field                                                          | 0m12.49s  || -0m00.65s
0m10.21s  | Testbit                                                                | 0m09.86s  || +0m00.35s
0m09.86s  | Reflection/Z/ArithmeticSimplifierInterp                                | 0m10.69s  || -0m00.83s
0m09.44s  | Reflection/Named/MapCastInterp                                         | 0m09.82s  || -0m00.38s
0m08.81s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m09.37s  || -0m00.55s
0m08.60s  | Assembly/GF25519                                                       | 0m08.66s  || -0m00.06s
0m08.58s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.77s  || -0m00.18s
0m08.53s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m08.34s  || +0m00.18s
0m08.41s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.77s  || -0m00.35s
0m08.26s  | Reflection/InlineWf                                                    | 0m08.59s  || -0m00.33s
0m07.54s  | Algebra/Ring                                                           | 0m08.04s  || -0m00.49s
0m07.43s  | MxDHRepChange                                                          | 0m07.10s  || +0m00.33s
0m07.15s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m07.09s  || +0m00.06s
0m07.00s  | NewBaseSystem                                                          | 0m07.16s  || -0m00.16s
0m06.51s  | Specific/GF1305                                                        | 0m06.52s  || -0m00.00s
0m06.09s  | Util/FixedWordSizesEquality                                            | 0m06.37s  || -0m00.28s
0m05.56s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.51s  || +0m00.04s
0m05.38s  | CompleteEdwardsCurve/Pre                                               | 0m05.38s  || +0m00.00s
0m05.28s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m05.15s  || +0m00.12s
0m05.24s  | Experiments/GenericFieldPow                                            | 0m05.54s  || -0m00.29s
0m05.01s  | Specific/SC25519                                                       | 0m05.38s  || -0m00.37s
0m04.93s  | Algebra/Field_test                                                     | 0m04.81s  || +0m00.12s
0m04.78s  | Reflection/InlineCastWf                                                | 0m04.94s  || -0m00.16s
0m04.10s  | Reflection/Z/Syntax/Equality                                           | 0m04.28s  || -0m00.18s
0m03.92s  | BaseSystemProofs                                                       | 0m03.90s  || +0m00.02s
0m03.75s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.94s  || -0m00.18s
0m03.72s  | CompleteEdwardsCurve/EdwardsMontgomery                                 | 0m03.69s  || +0m00.03s
0m03.72s  | Reflection/EtaWf                                                       | 0m03.71s  || +0m00.01s
0m03.60s  | Reflection/Named/CompileWf                                             | 0m04.01s  || -0m00.40s
0m03.58s  | SaturatedBaseSystem                                                    | 0m03.76s  || -0m00.17s
0m03.33s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.72s  || -0m00.39s
0m03.16s  | Reflection/LinearizeWf                                                 | 0m03.26s  || -0m00.09s
0m03.08s  | ModularArithmetic/ZBoundedZ                                            | 0m03.16s  || -0m00.08s
0m03.01s  | Specific/FancyMachine256/Montgomery                                    | 0m03.16s  || -0m00.15s
0m02.99s  | Reflection/Named/CompileInterp                                         | 0m03.24s  || -0m00.25s
0m02.92s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m03.06s  || -0m00.14s
0m02.92s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.15s  || -0m00.23s
0m02.90s  | Specific/FancyMachine256/Barrett                                       | 0m03.18s  || -0m00.28s
0m02.80s  | Spec/MontgomeryCurve                                                   | 0m03.05s  || -0m00.25s
0m02.77s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.75s  || +0m00.02s
0m02.75s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.81s  || -0m00.06s
0m02.64s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.62s  || +0m00.02s
0m02.54s  | Reflection/InlineInterp                                                | 0m02.60s  || -0m00.06s
0m02.48s  | Reflection/Named/ContextProperties                                     | 0m02.58s  || -0m00.10s
0m02.47s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.39s  || +0m00.08s
0m02.40s  | Reflection/TestCase                                                    | 0m02.60s  || -0m00.20s
0m02.35s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.40s  || -0m00.04s
0m02.35s  | Reflection/Z/Bounds/Relax                                              | 0m02.46s  || -0m00.10s
0m02.33s  | Reflection/Named/NameUtilProperties                                    | 0m02.40s  || -0m00.06s
0m02.15s  | Reflection/WfProofs                                                    | 0m02.26s  || -0m00.10s
0m02.00s  | Reflection/WfReflective                                                | 0m02.04s  || -0m00.04s
0m01.97s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m02.14s  || -0m00.17s
0m01.90s  | Specific/FancyMachine256/Core                                          | 0m01.98s  || -0m00.08s
0m01.89s  | Util/WordUtil                                                          | 0m01.96s  || -0m00.07s
0m01.88s  | Assembly/Evaluables                                                    | 0m01.82s  || +0m00.05s
0m01.62s  | WeierstrassCurve/Pre                                                   | 0m01.64s  || -0m00.01s
0m01.56s  | Reflection/Named/InterpretToPHOASWf                                    | 0m01.61s  || -0m00.05s
0m01.46s  | Assembly/Compile                                                       | 0m01.51s  || -0m00.05s
0m01.44s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.43s  || +0m00.01s
0m01.44s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.57s  || -0m00.13s
0m01.41s  | Algebra/Group                                                          | 0m01.87s  || -0m00.46s
0m01.40s  | Util/Tuple                                                             | 0m01.46s  || -0m00.06s
0m01.38s  | Reflection/MapCastInterp                                               | 0m01.38s  || +0m00.00s
0m01.31s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.05s  || +0m00.26s
0m01.26s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.28s  || -0m00.02s
0m01.16s  | Assembly/Conversions                                                   | 0m01.13s  || +0m00.03s
0m01.14s  | Reflection/Z/Bounds/Pipeline/Definition                                | 0m01.15s  || -0m00.01s
0m01.13s  | BaseSystem                                                             | 0m01.14s  || -0m00.01s
0m01.06s  | Reflection/SmartBoundInterp                                            | 0m01.07s  || -0m00.01s
0m01.04s  | Reflection/Named/InterpretToPHOASInterp                                | 0m00.99s  || +0m00.05s
0m01.01s  | Reflection/SmartCastWf                                                 | 0m00.94s  || +0m00.07s
0m01.01s  | Assembly/Pipeline                                                      | 0m01.02s  || -0m00.01s
0m01.01s  | Reflection/Relations                                                   | 0m01.06s  || -0m00.05s
0m00.97s  | Assembly/HL                                                            | 0m00.99s  || -0m00.02s
0m00.96s  | Algebra/IntegralDomain                                                 | 0m01.00s  || -0m00.04s
0m00.94s  | Assembly/LL                                                            | 0m01.02s  || -0m00.08s
0m00.92s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.91s  || +0m00.01s
0m00.90s  | Assembly/PhoasCommon                                                   | 0m00.87s  || +0m00.03s
0m00.89s  | Util/NumTheoryUtil                                                     | 0m00.92s  || -0m00.03s
0m00.87s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.96s  || -0m00.08s
0m00.84s  | Reflection/WfInversion                                                 | 0m00.88s  || -0m00.04s
0m00.83s  | Reflection/InlineCastInterp                                            | 0m00.85s  || -0m00.02s
0m00.81s  | Reflection/Named/CompileProperties                                     | 0m00.87s  || -0m00.05s
0m00.80s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.86s  || -0m00.05s
0m00.78s  | Karatsuba                                                              | 0m00.84s  || -0m00.05s
0m00.72s  | Util/PartiallyReifiedProp                                              | 0m00.73s  || -0m00.01s
0m00.72s  | Reflection/MultiSizeTest                                               | 0m00.72s  || +0m00.00s
0m00.69s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.72s  || -0m00.03s
0m00.68s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.61s  || +0m00.07s
0m00.68s  | Reflection/MapCastByDeBruijnInterp                                     | 0m00.76s  || -0m00.07s
0m00.68s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.80s  || -0m00.12s
0m00.68s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.72s  || -0m00.03s
0m00.67s  | Spec/EdDSA                                                             | 0m00.66s  || +0m00.01s
0m00.67s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.74s  || -0m00.06s
0m00.66s  | Reflection/Z/Bounds/Pipeline/ReflectiveTactics                         | 0m00.62s  || +0m00.04s
0m00.66s  | Util/IterAssocOp                                                       | 0m00.94s  || -0m00.27s
0m00.64s  | Encoding/ModularWordEncodingPre                                        | 0m00.73s  || -0m00.08s
0m00.63s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.77s  || -0m00.14s
0m00.62s  | Spec/ModularWordEncoding                                               | 0m00.66s  || -0m00.04s
0m00.61s  | Reflection/MapCastByDeBruijnWf                                         | 0m00.61s  || +0m00.00s
0m00.58s  | BoundedArithmetic/X86ToZLike                                           | 0m00.57s  || +0m00.01s
0m00.58s  | Reflection/Z/CNotations                                                | 0m00.56s  || +0m00.01s
0m00.57s  | Spec/WeierstrassCurve                                                  | 0m00.57s  || +0m00.00s
0m00.56s  | Spec/CompleteEdwardsCurve                                              | 0m00.59s  || -0m00.02s
0m00.56s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.58s  || -0m00.01s
0m00.56s  | Reflection/InterpByIsoProofs                                           | 0m00.60s  || -0m00.03s
0m00.55s  | Reflection/Named/WfInterp                                              | 0m00.57s  || -0m00.01s
0m00.55s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.57s  || -0m00.01s
0m00.54s  | Reflection/Named/FMapContext                                           | 0m00.70s  || -0m00.15s
0m00.54s  | Util/AdditionChainExponentiation                                       | 0m00.62s  || -0m00.07s
0m00.54s  | Reflection/SmartBoundWf                                                | 0m00.55s  || -0m00.01s
0m00.54s  | Reflection/WfReflectiveGen                                             | 0m00.54s  || +0m00.00s
0m00.54s  | BoundedArithmetic/Interface                                            | 0m00.56s  || -0m00.02s
0m00.52s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.46s  || +0m00.06s
0m00.52s  | Reflection/Z/JavaNotations                                             | 0m00.58s  || -0m00.05s
0m00.52s  | Reflection/Z/Syntax/Util                                               | 0m00.53s  || -0m00.01s
0m00.52s  | Util/CPSUtil                                                           | 0m00.57s  || -0m00.04s
0m00.51s  | Reflection/BoundByCastInterp                                           | 0m00.51s  || +0m00.00s
0m00.50s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.53s  || -0m00.03s
0m00.50s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.57s  || -0m00.06s
0m00.50s  | Reflection/InterpWfRel                                                 | 0m00.54s  || -0m00.04s
0m00.49s  | Reflection/Z/InlineInterp                                              | 0m00.37s  || +0m00.12s
0m00.49s  | Reflection/InputSyntax                                                 | 0m00.55s  || -0m00.06s
0m00.49s  | Util/Decidable                                                         | 0m00.48s  || +0m00.01s
0m00.48s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.39s  || +0m00.08s
0m00.48s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.48s  || +0m00.00s
0m00.47s  | BoundedArithmetic/Double/Core                                          | 0m00.50s  || -0m00.03s
0m00.47s  | Reflection/Z/Bounds/Pipeline                                           | 0m00.46s  || +0m00.00s
0m00.47s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.54s  || -0m00.07s
0m00.47s  | ModularArithmetic/ModularBaseSystemListZOperationsProofs               | 0m00.42s  || +0m00.04s
0m00.47s  | Util/NUtil                                                             | 0m00.50s  || -0m00.03s
0m00.47s  | Reflection/Z/Bounds/Interpretation                                     | 0m00.42s  || +0m00.04s
0m00.47s  | Reflection/Z/Reify                                                     | 0m00.49s  || -0m00.02s
0m00.46s  | BoundedArithmetic/StripCF                                              | 0m00.44s  || +0m00.02s
0m00.46s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.51s  || -0m00.04s
0m00.46s  | Reflection/Z/MapCastByDeBruijn                                         | 0m00.50s  || -0m00.03s
0m00.46s  | Reflection/Z/Bounds/MapCastByDeBruijnWf                                | 0m00.42s  || +0m00.04s
0m00.46s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.55s  || -0m00.09s
0m00.45s  | Util/HList                                                             | 0m00.50s  || -0m00.04s
0m00.44s  | Reflection/Z/Inline                                                    | 0m00.39s  || +0m00.04s
0m00.44s  | Reflection/InterpWf                                                    | 0m00.55s  || -0m00.11s
0m00.44s  | Reflection/Z/Syntax                                                    | 0m00.46s  || -0m00.02s
0m00.44s  | Reflection/Z/ArithmeticSimplifier                                      | 0m00.47s  || -0m00.02s
0m00.44s  | Reflection/Named/DeadCodeElimination                                   | 0m00.36s  || +0m00.08s
0m00.44s  | ModularArithmetic/ZBounded                                             | 0m00.49s  || -0m00.04s
0m00.43s  | ModularArithmetic/Pre                                                  | 0m00.44s  || -0m00.01s
0m00.42s  | ModularArithmetic/Montgomery/Z                                         | 0m00.39s  || +0m00.02s
0m00.42s  | Reflection/Z/Bounds/MapCastByDeBruijnInterp                            | 0m00.43s  || -0m00.01s
0m00.42s  | Util/ZRange                                                            | 0m00.42s  || +0m00.00s
0m00.42s  | Reflection/Z/MapCastByDeBruijnInterp                                   | 0m00.46s  || -0m00.04s
0m00.41s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.45s  || -0m00.04s
0m00.41s  | Reflection/Z/Bounds/MapCastByDeBruijn                                  | 0m00.50s  || -0m00.09s
0m00.40s  | Reflection/Z/MapCastByDeBruijnWf                                       | 0m00.50s  || -0m00.09s
0m00.40s  | Reflection/Z/InlineWf                                                  | 0m00.42s  || -0m00.01s
0m00.40s  | Reflection/Z/Bounds/Pipeline/OutputType                                | 0m00.38s  || +0m00.02s
0m00.40s  | ModularArithmetic/Pow2Base                                             | 0m00.43s  || -0m00.02s
0m00.40s  | Reflection/Named/PositiveContext/DefaultsProperties                    | 0m00.52s  || -0m00.12s
0m00.40s  | Reflection/MapCastByDeBruijn                                           | 0m00.39s  || +0m00.01s
0m00.39s  | Reflection/Z/Bounds/Pipeline/Glue                                      | 0m00.46s  || -0m00.07s
0m00.39s  | Reflection/Named/PositiveContext/Defaults                              | 0m00.40s  || -0m00.01s
0m00.39s  | Reflection/Named/ContextDefinitions                                    | 0m00.37s  || +0m00.02s
0m00.38s  | Reflection/Z/FoldTypes                                                 | 0m00.38s  || +0m00.00s
0m00.38s  | Reflection/Z/HexNotationConstants                                      | 0m00.42s  || -0m00.03s
0m00.38s  | Reflection/Z/OpInversion                                               | 0m00.37s  || +0m00.01s
0m00.38s  | ModularArithmetic/ModularBaseSystemListZOperations                     | 0m00.41s  || -0m00.02s
0m00.38s  | Reflection/Named/EstablishLiveness                                     | 0m00.38s  || +0m00.00s
0m00.38s  | Reflection/Named/RegisterAssign                                        | 0m00.38s  || +0m00.00s
0m00.38s  | Reflection/Reify                                                       | 0m00.40s  || -0m00.02s
0m00.37s  | ModularArithmetic/ModularBaseSystemWord                                | 0m00.38s  || -0m00.01s
0m00.36s  | Reflection/Named/InterpretToPHOAS                                      | 0m00.45s  || -0m00.09s
0m00.36s  | Reflection/Named/Syntax                                                | 0m00.35s  || +0m00.01s
0m00.36s  | BoundedArithmetic/Eta                                                  | 0m00.42s  || -0m00.06s
0m00.35s  | Reflection/Named/Compile                                               | 0m00.34s  || +0m00.00s
0m00.35s  | Reflection/MapCastWf                                                   | 0m00.31s  || +0m00.03s
0m00.35s  | Reflection/Named/SmartMap                                              | 0m00.36s  || -0m00.01s
0m00.35s  | Util/BoundedWord                                                       | 0m00.40s  || -0m00.05s
0m00.35s  | Spec/ModularArithmetic                                                 | 0m00.36s  || -0m00.01s
0m00.34s  | Reflection/Named/ContextOn                                             | 0m00.34s  || +0m00.00s
0m00.34s  | Reflection/FilterLive                                                  | 0m00.32s  || +0m00.02s
0m00.34s  | Reflection/Named/MapCast                                               | 0m00.37s  || -0m00.02s
0m00.33s  | Reflection/Named/PositiveContext                                       | 0m00.39s  || -0m00.06s
0m00.33s  | Algebra/ScalarMult                                                     | 0m00.56s  || -0m00.23s
0m00.32s  | Reflection/Z/BinaryNotationConstants                                   | 0m00.35s  || -0m00.02s
0m00.32s  | Reflection/Tuple                                                       | 0m00.38s  || -0m00.06s
0m00.32s  | Reflection/Named/ContextProperties/Tactics                             | 0m00.48s  || -0m00.15s
0m00.32s  | Reflection/Named/IdContext                                             | 0m00.33s  || -0m00.01s
0m00.31s  | Reflection/Named/Wf                                                    | 0m00.38s  || -0m00.07s
0m00.30s  | Reflection/MultiSizeTest2                                              | 0m00.34s  || -0m00.04s
0m00.29s  | Reflection/ExprInversion                                               | 0m00.26s  || +0m00.02s
0m00.29s  | Spec/MxDH                                                              | 0m00.43s  || -0m00.14s
0m00.26s  | Algebra/Monoid                                                         | 0m00.51s  || -0m00.25s
0m00.26s  | Util/Sum                                                               | 0m00.34s  || -0m00.08s
0m00.24s  | Algebra                                                                | 0m00.43s  || -0m00.19s
0m00.23s  | Reflection/Equality                                                    | 0m00.25s  || -0m00.01s
0m00.22s  | Reflection/CommonSubexpressionElimination                              | 0m00.17s  || +0m00.04s
0m00.21s  | Reflection/SmartMap                                                    | 0m00.23s  || -0m00.02s
0m00.20s  | Reflection/EtaInterp                                                   | 0m00.22s  || -0m00.01s
0m00.20s  | Reflection/BoundByCastWf                                               | 0m00.12s  || +0m00.08s
0m00.20s  | Reflection/LinearizeInterp                                             | 0m00.23s  || -0m00.03s
0m00.18s  | Util/LetInMonad                                                        | 0m00.19s  || -0m00.01s
0m00.16s  | Reflection/InterpProofs                                                | 0m00.18s  || -0m00.01s
0m00.13s  | Util/Option                                                            | 0m00.14s  || -0m00.01s
0m00.13s  | Reflection/Wf                                                          | 0m00.12s  || +0m00.01s
0m00.12s  | Reflection/RewriterWf                                                  | 0m00.19s  || -0m00.07s
0m00.08s  | Reflection/Conversion                                                  | 0m00.08s  || +0m00.00s
0m00.08s  | Reflection/Named/NameUtil                                              | 0m00.12s  || -0m00.03s
0m00.07s  | Reflection/Inline                                                      | 0m00.04s  || +0m00.03s
0m00.06s  | Reflection/TypeInversion                                               | 0m00.08s  || -0m00.02s
0m00.06s  | Reflection/SmartBound                                                  | 0m00.06s  || +0m00.00s
0m00.06s  | Reflection/InlineCast                                                  | 0m00.06s  || +0m00.00s
0m00.06s  | Util/Tactics                                                           | 0m00.07s  || -0m00.01s
0m00.06s  | Reflection/RewriterInterp                                              | 0m00.05s  || +0m00.00s
0m00.06s  | Reflection/MapCast                                                     | 0m00.06s  || +0m00.00s
0m00.05s  | Reflection/TypeUtil                                                    | 0m00.04s  || +0m00.01s
0m00.04s  | Reflection/Syntax                                                      | 0m00.09s  || -0m00.05s
0m00.04s  | Reflection/FoldTypes                                                   | 0m00.05s  || -0m00.01s
0m00.04s  | Reflection/Linearize                                                   | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/Rewriter                                                    | 0m00.03s  || +0m00.01s
0m00.04s  | Reflection/Map                                                         | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Tactics/OnSubterms                                                |    N/A    || +0m00.04s
0m00.04s  | Reflection/CountLets                                                   | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/SmartCast                                                   | 0m00.04s  || +0m00.00s
0m00.04s  | Util/LetIn                                                             | 0m00.07s  || -0m00.03s
0m00.04s  | Reflection/Eta                                                         | 0m00.05s  || -0m00.01s
0m00.04s  | Reflection/BoundByCast                                                 | 0m00.06s  || -0m00.01s
0m00.03s  | Reflection/SmartCastInterp                                             | 0m00.05s  || -0m00.02s
0m00.03s  | Util/Tactics/SubstEvars                                                |    N/A    || +0m00.03s
0m00.03s  | Reflection/InterpByIso                                                 | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/Forward                                                   |    N/A    || +0m00.03s
0m00.03s  | Util/Tactics/BreakMatch                                                | 0m00.02s  || +0m00.00s
0m00.03s  | Reflection/RenameBinders                                               | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/ConvoyDestruct                                            |    N/A    || +0m00.03s
0m00.02s  | Util/Tactics/SideConditionsBeforeToAfter                               |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/Revert                                                    |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/Test                                                      |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/SetEvars                                                  |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/SetoidSubst                                               |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/DestructTrivial                                           |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/ESpecialize                                               |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/SimplifyProjections                                       |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/Not                                                       |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/Contains                                                  |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/SimplifyRepeatedIfs                                       |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/ClearDuplicates                                           |    N/A    || +0m00.02s
0m00.02s  | Util/Tactics/DebugPrint                                                |    N/A    || +0m00.02s
0m00.01s  | Util/Tactics/GetGoal                                                   |    N/A    || +0m00.01s

1 files changed, 18 insertions, 315 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index d6ab637aa..88dcb0aa8 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -1,331 +1,34 @@
 (** * Generic Tactics *)
 Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.Tactics.BreakMatch.
+Require Export Crypto.Util.Tactics.Contains.
+Require Export Crypto.Util.Tactics.ConvoyDestruct.
+Require Export Crypto.Util.Tactics.ClearDuplicates.
 Require Export Crypto.Util.Tactics.Head.
+Require Export Crypto.Util.Tactics.DebugPrint.
 Require Export Crypto.Util.Tactics.DestructHyps.
 Require Export Crypto.Util.Tactics.DestructHead.
+Require Export Crypto.Util.Tactics.DestructTrivial.
 Require Export Crypto.Util.Tactics.DoWithHyp.
+Require Export Crypto.Util.Tactics.ESpecialize.
 Require Export Crypto.Util.Tactics.ETransitivity.
 Require Export Crypto.Util.Tactics.EvarExists.
+Require Export Crypto.Util.Tactics.Forward.
+Require Export Crypto.Util.Tactics.GetGoal.
+Require Export Crypto.Util.Tactics.OnSubterms.
+Require Export Crypto.Util.Tactics.Not.
+Require Export Crypto.Util.Tactics.Revert.
 Require Export Crypto.Util.Tactics.RewriteHyp.
+Require Export Crypto.Util.Tactics.SetEvars.
+Require Export Crypto.Util.Tactics.SetoidSubst.
+Require Export Crypto.Util.Tactics.SideConditionsBeforeToAfter.
+Require Export Crypto.Util.Tactics.SimplifyProjections.
+Require Export Crypto.Util.Tactics.SimplifyRepeatedIfs.
 Require Export Crypto.Util.Tactics.SpecializeBy.
 Require Export Crypto.Util.Tactics.SplitInContext.
+Require Export Crypto.Util.Tactics.SubstEvars.
 Require Export Crypto.Util.Tactics.SubstLet.
+Require Export Crypto.Util.Tactics.Test.
 Require Export Crypto.Util.Tactics.UnifyAbstractReflexivity.
 Require Export Crypto.Util.Tactics.UniquePose.
 Require Export Crypto.Util.Tactics.VM.
-
-(** Test if a tactic succeeds, but always roll-back the results *)
-Tactic Notation "test" tactic3(tac) :=
-  try (first [ tac | fail 2 tac "does not succeed" ]; fail 0 tac "succeeds"; [](* test for [t] solved all goals *)).
-
-(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
-Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds").
-
-Ltac get_goal :=
-  match goal with |- ?G => G end.
-
-(** [contains x expr] succeeds iff [x] appears in [expr] *)
-Ltac contains search_for in_term :=
-  idtac;
-  lazymatch in_term with
-  | appcontext[search_for] => idtac
-  end.
-
-Ltac debuglevel := constr:(0%nat).
-
-Ltac solve_debugfail tac :=
-  solve [tac] ||
-        ( let dbg := debuglevel in
-          match dbg with
-          | O => idtac
-          | _ => match goal with |- ?G => idtac "couldn't prove" G end
-          end;
-          fail).
-
-Ltac set_evars :=
-  repeat match goal with
-         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
-         end.
-
-Ltac subst_evars :=
-  repeat match goal with
-         | [ e := ?E |- _ ] => is_evar E; subst e
-         end.
-
-Ltac free_in x y :=
-  idtac;
-  match y with
-    | appcontext[x] => fail 1 x "appears in" y
-    | _ => idtac
-  end.
-
-Ltac setoid_subst'' R x :=
-  is_var x;
-  match goal with
-  | [ H : R x ?y |- _ ]
-    => free_in x y; rewrite ?H in *; clear x H
-  | [ H : R ?y x |- _ ]
-    => free_in x y; rewrite <- ?H in *; clear x H
-  end.
-
-Ltac setoid_subst' x :=
-  is_var x;
-  match goal with
-  | [ H : ?R x _ |- _ ] => setoid_subst'' R x
-  | [ H : ?R _ x |- _ ] => setoid_subst'' R x
-  end.
-
-Ltac setoid_subst_rel' R :=
-  idtac;
-  match goal with
-  | [ H : R ?x _ |- _ ] => setoid_subst'' R x
-  | [ H : R _ ?x |- _ ] => setoid_subst'' R x
-  end.
-
-Ltac setoid_subst_rel R := repeat setoid_subst_rel' R.
-
-Ltac setoid_subst_all :=
-  repeat match goal with
-         | [ H : ?R ?x ?y |- _ ] => is_var x; setoid_subst'' R x
-         | [ H : ?R ?x ?y |- _ ] => is_var y; setoid_subst'' R y
-         end.
-
-Tactic Notation "setoid_subst" ident(x) := setoid_subst' x.
-Tactic Notation "setoid_subst" := setoid_subst_all.
-
-Ltac destruct_trivial_step :=
-  match goal with
-  | [ H : unit |- _ ] => clear H || destruct H
-  | [ H : True |- _ ] => clear H || destruct H
-  end.
-Ltac destruct_trivial := repeat destruct_trivial_step.
-
-Ltac clear_duplicates_step :=
-  match goal with
-  | [ H : ?T, H' : ?T |- _ ] => clear H'
-  | [ H := ?T, H' := ?T |- _ ] => clear H'
-  end.
-Ltac clear_duplicates := repeat clear_duplicates_step.
-
-
-(** given a [matcher] that succeeds on some hypotheses and fails on
-    others, destruct any matching hypotheses, and then execute [tac]
-    after each [destruct].
-
-    The [tac] part exists so that you can, e.g., [simpl in *], to
-    speed things up. *)
-Ltac do_one_match_then matcher do_tac tac :=
-  idtac;
-  match goal with
-  | [ H : ?T |- _ ]
-    => matcher T; do_tac H;
-       try match type of H with
-           | T => clear H
-           end;
-       tac
-  end.
-
-Ltac do_all_matches_then matcher do_tac tac :=
-  repeat do_one_match_then matcher do_tac tac.
-
-Ltac destruct_all_matches_then matcher tac :=
-  do_all_matches_then matcher ltac:(fun H => destruct H) tac.
-Ltac destruct_one_match_then matcher tac :=
-  do_one_match_then matcher ltac:(fun H => destruct H) tac.
-
-Ltac inversion_all_matches_then matcher tac :=
-  do_all_matches_then matcher ltac:(fun H => inversion H; subst) tac.
-Ltac inversion_one_match_then matcher tac :=
-  do_one_match_then matcher ltac:(fun H => inversion H; subst) tac.
-
-Ltac destruct_all_matches matcher :=
-  destruct_all_matches_then matcher ltac:( simpl in * ).
-Ltac destruct_one_match matcher := destruct_one_match_then matcher ltac:( simpl in * ).
-Ltac destruct_all_matches' matcher := destruct_all_matches_then matcher idtac.
-
-Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( simpl in * ).
-Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ).
-Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac.
-
-(** If [tac_in H] operates in [H] and leaves side-conditions before
-    the original goal, then
-    [side_conditions_before_to_side_conditions_after tac_in H] does
-    the same thing to [H], but leaves side-conditions after the
-    original goal. *)
-Ltac side_conditions_before_to_side_conditions_after tac_in H :=
-  let HT := type of H in
-  let HTT := type of HT in
-  let H' := fresh in
-  rename H into H';
-  let HT' := fresh in
-  evar (HT' : HTT);
-  cut HT';
-  [ subst HT'; intro H
-  | tac_in H';
-    [ ..
-    | subst HT'; eexact H' ] ];
-  instantiate; (* required in 8.4 for the [move] to succeed, because evar dependencies *)
-  [ (* We preserve the order of the hypotheses.  We need to do this
-       here, after evars are instantiated, and not above. *)
-    move H after H'; clear H'
-  | .. ].
-
-(** Execute [progress tac] on all subterms of the goal.  Useful for things like [ring_simplify]. *)
-Ltac tac_on_subterms tac :=
-  repeat match goal with
-         | [ |- 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.
-
-Ltac simplify_repeated_ifs_step :=
-  match goal with
-  | [ |- context G[if ?b then ?x else ?y] ]
-    => let x' := match x with
-                 | context x'[b] => let x'' := context x'[true] in x''
-                 end in
-       let G' := context G[if b then x' else y] in
-       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
-  | [ |- context G[if ?b then ?x else ?y] ]
-    => let y' := match y with
-                 | context y'[b] => let y'' := context y'[false] in y''
-                 end in
-       let G' := context G[if b then x else y'] in
-       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
-  end.
-Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step.
-
-(** Like [specialize] but allows holes that get filled with evars. *)
-Tactic Notation "especialize" open_constr(H) := specialize H.
-
-(** [forward H] specializes non-dependent binders in a hypothesis [H]
-    with side-conditions.  Side-conditions come after the main goal,
-    like with [replace] and [rewrite].
-
-    [eforward H] is like [forward H], but also specializes dependent
-    binders with evars.
-
-    Both tactics do nothing on hypotheses they cannot handle. *)
-Ltac forward_step H :=
-  match type of H with
-  | ?A -> ?B => let a := fresh in cut A; [ intro a; specialize (H a); clear a | ]
-  end.
-Ltac eforward_step H :=
-  match type of H with
-  | _ => forward_step H
-  | forall x : ?A, _
-    => let x_or_fresh := fresh x in
-       evar (x_or_fresh : A);
-       specialize (H x_or_fresh); subst x_or_fresh
-  end.
-Ltac forward H := try (forward_step H; [ forward H | .. ]).
-Ltac eforward H := try (eforward_step H; [ eforward H | .. ]).
-
-(** [simplify_projections] reduces terms of the form [fst (_, _)] (for
-    any projection from [prod], [sig], [sigT], or [and]) *)
-Ltac pre_simplify_projection proj proj' uproj' :=
-  pose proj as proj';
-  pose proj as uproj';
-  unfold proj in uproj';
-  change proj with proj'.
-Ltac do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct :=
-  change proj' with uproj' at 1;
-  lazymatch goal with
-  | [ |- appcontext[uproj' _ _ (construct _ _ _ _)] ]
-    => cbv beta iota delta [uproj']
-  | _ => change uproj' with proj
-  end.
-Ltac do_simplify_projection_2Targ_4carg proj proj' uproj' construct :=
-  repeat do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct.
-Ltac simplify_projection_2Targ_4carg proj construct :=
-  let proj' := fresh "proj" in
-  let uproj' := fresh "proj" in
-  pre_simplify_projection proj proj' uproj';
-  do_simplify_projection_2Targ_4carg proj proj' uproj' construct;
-  clear proj' uproj'.
-
-Ltac simplify_projections :=
-  repeat (simplify_projection_2Targ_4carg @fst @pair
-          || simplify_projection_2Targ_4carg @snd @pair
-          || simplify_projection_2Targ_4carg @proj1_sig @exist
-          || simplify_projection_2Targ_4carg @proj2_sig @exist
-          || simplify_projection_2Targ_4carg @projT1 @existT
-          || simplify_projection_2Targ_4carg @projT2 @existT
-          || simplify_projection_2Targ_4carg @proj1 @conj
-          || simplify_projection_2Targ_4carg @proj2 @conj).
-
-(** constr-based [idtac] *)
-Class cidtac {T} (msg : T) := Build_cidtac : True.
-Hint Extern 0 (cidtac ?msg) => idtac msg; exact I : typeclass_instances.
-(** constr-based [idtac] *)
-Class cidtac2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cidtac2 : True.
-Hint Extern 0 (cidtac2 ?msg1 ?msg2) => idtac msg1 msg2; exact I : typeclass_instances.
-Class cidtac3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cidtac3 : True.
-Hint Extern 0 (cidtac3 ?msg1 ?msg2 ?msg3) => idtac msg1 msg2 msg3; exact I : typeclass_instances.
-
-Class cfail {T} (msg : T) := Build_cfail : True.
-Hint Extern 0 (cfail ?msg) => idtac "Error:" msg; exact I : typeclass_instances.
-Class cfail2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cfail2 : True.
-Hint Extern 0 (cfail2 ?msg1 ?msg2) => idtac "Error:" msg1 msg2; exact I : typeclass_instances.
-Class cfail3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cfail3 : True.
-Hint Extern 0 (cfail3 ?msg1 ?msg2 ?msg3) => idtac "Error:" msg1 msg2 msg3; exact I : typeclass_instances.
-
-Ltac cidtac msg := constr:(_ : cidtac msg).
-Ltac cidtac2 msg1 msg2 := constr:(_ : cidtac2 msg1 msg2).
-Ltac cidtac3 msg1 msg2 msg3 := constr:(_ : cidtac2 msg1 msg2 msg3).
-Ltac cfail msg := let dummy := constr:(_ : cfail msg) in constr:(I : I).
-Ltac cfail2 msg1 msg2 := let dummy := constr:(_ : cfail2 msg1 msg2) in constr:(I : I).
-Ltac cfail3 msg1 msg2 msg3 := let dummy := constr:(_ : cfail2 msg1 msg2 msg3) in constr:(I : I).
-
-Ltac idtac_goal := lazymatch goal with |- ?G => idtac "Goal:" G end.
-Ltac idtac_context :=
-  try (repeat match goal with H : _ |- _ => revert H end;
-       idtac_goal;
-       lazymatch goal with |- ?G => idtac "Context:" G end;
-       fail).
-
-(** Destruct the convoy pattern ([match e as x return x = e -> _ with _ => _ end eq_refl] *)
-Ltac convoy_destruct_gen T change_in :=
-  let e' := fresh in
-  let H' := fresh in
-  match T with
-  | context G[?f eq_refl]
-    => match f with
-       | match ?e with _ => _ end
-         => pose e as e';
-            match f with
-            | context F[e]
-              => let F' := context F[e'] in
-                 first [ pose (eq_refl : e = e') as H';
-                         let G' := context G[F' H'] in
-                         change_in G';
-                         clearbody H' e'
-                       | pose (eq_refl : e' = e) as H';
-                         let G' := context G[F' H'] in
-                         change_in G';
-                         clearbody H' e' ]
-            end
-       end;
-       destruct e'
-  end.
-
-Ltac convoy_destruct_in H :=
-  let T := type of H in
-  convoy_destruct_gen T ltac:(fun T' => change T' in H).
-Ltac convoy_destruct :=
-  let T := get_goal in
-  convoy_destruct_gen T ltac:(fun T' => change T').