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

19 files changed, 269 insertions, 0 deletions

diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v
index 486d3ef92..f03823a92 100644
--- a/src/Util/Tactics/BreakMatch.v
+++ b/src/Util/Tactics/BreakMatch.v
@@ -117,4 +117,10 @@ Ltac break_innermost_match_step :=
                                   | appcontext[match _ with _ => _ end] => fail
                                   | _ => idtac
                                   end).
+Ltac break_innermost_match_hyps_step :=
+  break_match_hyps_step ltac:(fun v => lazymatch v with
+                                       | appcontext[match _ with _ => _ end] => fail
+                                       | _ => idtac
+                                       end).
 Ltac break_innermost_match := repeat break_innermost_match_step.
+Ltac break_innermost_match_hyps := repeat break_innermost_match_hyps_step.
diff --git a/src/Util/Tactics/ClearDuplicates.v b/src/Util/Tactics/ClearDuplicates.v
new file mode 100644
index 000000000..471f9c1a3
--- /dev/null
+++ b/src/Util/Tactics/ClearDuplicates.v
@@ -0,0 +1,6 @@
+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.
diff --git a/src/Util/Tactics/Contains.v b/src/Util/Tactics/Contains.v
new file mode 100644
index 000000000..aa4fddac2
--- /dev/null
+++ b/src/Util/Tactics/Contains.v
@@ -0,0 +1,13 @@
+(** [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 free_in x y :=
+  idtac;
+  match y with
+    | appcontext[x] => fail 1 x "appears in" y
+    | _ => idtac
+  end.
diff --git a/src/Util/Tactics/ConvoyDestruct.v b/src/Util/Tactics/ConvoyDestruct.v
new file mode 100644
index 000000000..5ed556142
--- /dev/null
+++ b/src/Util/Tactics/ConvoyDestruct.v
@@ -0,0 +1,33 @@
+Require Import Crypto.Util.Tactics.GetGoal.
+
+(** 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').
diff --git a/src/Util/Tactics/DebugPrint.v b/src/Util/Tactics/DebugPrint.v
new file mode 100644
index 000000000..e1650f170
--- /dev/null
+++ b/src/Util/Tactics/DebugPrint.v
@@ -0,0 +1,40 @@
+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).
+
+(** 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).
diff --git a/src/Util/Tactics/DestructTrivial.v b/src/Util/Tactics/DestructTrivial.v
new file mode 100644
index 000000000..716e953fb
--- /dev/null
+++ b/src/Util/Tactics/DestructTrivial.v
@@ -0,0 +1,6 @@
+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.
diff --git a/src/Util/Tactics/ESpecialize.v b/src/Util/Tactics/ESpecialize.v
new file mode 100644
index 000000000..288bc8607
--- /dev/null
+++ b/src/Util/Tactics/ESpecialize.v
@@ -0,0 +1,2 @@
+(** Like [specialize] but allows holes that get filled with evars. *)
+Tactic Notation "especialize" open_constr(H) := specialize H.
diff --git a/src/Util/Tactics/Forward.v b/src/Util/Tactics/Forward.v
new file mode 100644
index 000000000..63ac6ef38
--- /dev/null
+++ b/src/Util/Tactics/Forward.v
@@ -0,0 +1,22 @@
+(** [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 | .. ]).
diff --git a/src/Util/Tactics/GetGoal.v b/src/Util/Tactics/GetGoal.v
new file mode 100644
index 000000000..2d99ca31e
--- /dev/null
+++ b/src/Util/Tactics/GetGoal.v
@@ -0,0 +1,2 @@
+Ltac get_goal :=
+  match goal with |- ?G => G end.
diff --git a/src/Util/Tactics/Not.v b/src/Util/Tactics/Not.v
new file mode 100644
index 000000000..09985ad73
--- /dev/null
+++ b/src/Util/Tactics/Not.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Util.Tactics.Test.
+
+(** [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").
diff --git a/src/Util/Tactics/OnSubterms.v b/src/Util/Tactics/OnSubterms.v
new file mode 100644
index 000000000..0aabf80c8
--- /dev/null
+++ b/src/Util/Tactics/OnSubterms.v
@@ -0,0 +1,6 @@
+(** 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.
diff --git a/src/Util/Tactics/Revert.v b/src/Util/Tactics/Revert.v
new file mode 100644
index 000000000..5f549025d
--- /dev/null
+++ b/src/Util/Tactics/Revert.v
@@ -0,0 +1,13 @@
+(** 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.
diff --git a/src/Util/Tactics/SetEvars.v b/src/Util/Tactics/SetEvars.v
new file mode 100644
index 000000000..471d61f60
--- /dev/null
+++ b/src/Util/Tactics/SetEvars.v
@@ -0,0 +1,4 @@
+Ltac set_evars :=
+  repeat match goal with
+         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
+         end.
diff --git a/src/Util/Tactics/SetoidSubst.v b/src/Util/Tactics/SetoidSubst.v
new file mode 100644
index 000000000..4ccf910ed
--- /dev/null
+++ b/src/Util/Tactics/SetoidSubst.v
@@ -0,0 +1,35 @@
+Require Import Crypto.Util.Tactics.Contains.
+
+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.
diff --git a/src/Util/Tactics/SideConditionsBeforeToAfter.v b/src/Util/Tactics/SideConditionsBeforeToAfter.v
new file mode 100644
index 000000000..0067d53f5
--- /dev/null
+++ b/src/Util/Tactics/SideConditionsBeforeToAfter.v
@@ -0,0 +1,22 @@
+(** 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'
+  | .. ].
diff --git a/src/Util/Tactics/SimplifyProjections.v b/src/Util/Tactics/SimplifyProjections.v
new file mode 100644
index 000000000..f9b319057
--- /dev/null
+++ b/src/Util/Tactics/SimplifyProjections.v
@@ -0,0 +1,32 @@
+(** [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).
diff --git a/src/Util/Tactics/SimplifyRepeatedIfs.v b/src/Util/Tactics/SimplifyRepeatedIfs.v
new file mode 100644
index 000000000..54d79ee48
--- /dev/null
+++ b/src/Util/Tactics/SimplifyRepeatedIfs.v
@@ -0,0 +1,16 @@
+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.
diff --git a/src/Util/Tactics/SubstEvars.v b/src/Util/Tactics/SubstEvars.v
new file mode 100644
index 000000000..5e1765c2f
--- /dev/null
+++ b/src/Util/Tactics/SubstEvars.v
@@ -0,0 +1,4 @@
+Ltac subst_evars :=
+  repeat match goal with
+         | [ e := ?E |- _ ] => is_evar E; subst e
+         end.
diff --git a/src/Util/Tactics/Test.v b/src/Util/Tactics/Test.v
new file mode 100644
index 000000000..63529bbfc
--- /dev/null
+++ b/src/Util/Tactics/Test.v
@@ -0,0 +1,3 @@
+(** 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 *)).