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

5 files changed, 24 insertions, 18 deletions

diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index ebc92c0e5..f35e2c1cc 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -1,4 +1,6 @@
-Require Import Crypto.Util.Relations Crypto.Util.Tactics Crypto.Util.Notations.
+Require Import Crypto.Util.Relations Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.DebugPrint.
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
 Require Coq.setoid_ring.Field_theory.
@@ -243,7 +245,7 @@ Ltac inequalities_to_inverse_equations fld :=
              unique pose proof (right_multiplicative_inverse(H:=fld) _ H)
            | not (eq zero ?d) =>
              unique pose proof (right_multiplicative_inverse(H:=fld) _ (symmetry(R:=fun a b => not (eq a b)) H))
-           | not (eq ?x ?y) => 
+           | not (eq ?x ?y) =>
              unique pose proof (right_multiplicative_inverse(H:=fld) _ (Ring.neq_sub_neq_zero _ _ H))
            end
          end.
@@ -261,7 +263,7 @@ Ltac inverses_to_conditional_equations fld :=
   repeat match goal with
          | |- context[inv ?d] =>
            unique_pose_implication constr:(right_multiplicative_inverse(H:=fld) d)
-         | H: context[inv ?d] |- _ => 
+         | H: context[inv ?d] |- _ =>
            unique_pose_implication constr:(right_multiplicative_inverse(H:=fld) d)
          end.
 
@@ -324,4 +326,4 @@ Section FieldSquareRoot.
     eapply zero_product_zero_factor.
     fsatz.
   Qed.
-End FieldSquareRoot.
\ No newline at end of file
+End FieldSquareRoot.
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index c1c514171..b053fc844 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.Morphisms Crypto.Util.Relations Crypto.Util.Tactics.
+Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*).
 Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
 
 Section BasicProperties.
@@ -213,4 +213,4 @@ Section HomomorphismComposition.
   Global Instance is_homomorphism_compose_refl
     : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
     := is_homomorphism_compose (fun x => reflexivity _).
-End HomomorphismComposition.
\ No newline at end of file
+End HomomorphismComposition.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index f58874710..083c10242 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -1,6 +1,9 @@
-Require Import Crypto.Util.Tactics Crypto.Util.Relations.
+Require Coq.setoid_ring.Integral_domain.
+Require Crypto.Tactics.Algebra_syntax.Nsatz.
 Require Import Crypto.Util.Factorize.
 Require Import Crypto.Algebra Crypto.Algebra.Ring.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.BreakMatch.
 
 Module IntegralDomain.
   Section IntegralDomain.
@@ -25,7 +28,7 @@ Module IntegralDomain.
       Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
       Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
       Local Infix "+" := add.  Local Infix "-" := sub. Local Infix "*" := mul.
-      
+
       Inductive coef :=
       | Coef_one
       | Coef_opp (_:coef)
@@ -62,7 +65,7 @@ Module IntegralDomain.
 
       Section WithChar.
         Context C (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C) (HC: Pos.lt xH C).
-        
+
         Definition is_factor_nonzero (n:N) : bool :=
           match n with N0 => false | N.pos p => BinPos.Pos.ltb p C end.
         Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true)
@@ -79,7 +82,7 @@ Module IntegralDomain.
           { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism of_Z.
             eapply Ring.nonzero_product_iff_nonzero_factor; eauto. }
         Qed.
-          
+
         Definition is_constant_nonzero (z:Z) : bool :=
           match factorize_or_fail (Z.abs_N z) with
           | Some factors => List.forallb is_factor_nonzero factors
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
index f71efff3e..565058cf7 100644
--- a/src/Algebra/Monoid.v
+++ b/src/Algebra/Monoid.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Algebra.
 
 Section Monoid.
@@ -57,4 +57,4 @@ Section Homomorphism.
       is_homomorphism_phi_proper : Proper (respectful EQ eq) phi
     }.
   Global Existing Instance is_homomorphism_phi_proper.
-End Homomorphism.
\ No newline at end of file
+End Homomorphism.
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index 5c1cb1603..2b0e1ba80 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -1,8 +1,13 @@
+Require Coq.setoid_ring.Ncring.
+Require Coq.setoid_ring.Cring.
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.OnSubterms.
+Require Import Crypto.Util.Tactics.Revert.
 Require Import Crypto.Algebra Crypto.Algebra.Group Crypto.Algebra.Monoid.
 Require Coq.ZArith.ZArith Coq.PArith.PArith.
 
+
 Section Ring.
   Context {T eq zero one opp add sub mul} `{@ring T eq zero one opp add sub mul}.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
@@ -86,10 +91,6 @@ Section Ring.
     forall x y : T, not (eq (mul x y) zero) <-> (not (eq x zero) /\ not (eq y zero)).
   Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed.
 
-  Lemma nonzero_hypothesis_to_goal {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
-    forall x y : T, (not (eq x zero) -> eq y zero) <-> (eq (mul x y) zero).
-  Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed.
-
   Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq.
   Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops.
   Proof.
@@ -434,4 +435,4 @@ 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.
\ No newline at end of file
+Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all.