make elliptic curve proofs faster and split them into files

fix EdwardsMontgomery

try to speed up Weierstrass proof

--amend

Conflicts fixed by Jason Gross; timing diff added by Jason Gross

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

1 files changed, 11 insertions, 5 deletions

diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index e7e8ce471..2703ef108 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -11,7 +11,6 @@ Local Open Scope type_scope.
 
 Class Decidable (P : Prop) := dec : {P} + {~P}.
 Arguments dec _%type_scope {_}.
-
 Notation DecidableRel R := (forall x y, Decidable (R x y)).
 
 Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10.
@@ -85,7 +84,6 @@ Lemma dec_not {A} `{Decidable A} : Decidable (~A).
 Proof. solve_decidable_transparent. Defined.
 (** Disallow infinite loops of dec_not *)
 Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances.
-
 Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined.
 Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined.
 Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined.
@@ -110,8 +108,6 @@ Global Instance dec_le_Z : DecidableRel BinInt.Z.le := ZArith_dec.Z_le_dec.
 Global Instance dec_gt_Z : DecidableRel BinInt.Z.gt := ZArith_dec.Z_gt_dec.
 Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec.
 
-Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec.
-
 Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B}
        {HD : Decidable (P (fst x) (snd x))}
   : Decidable (let '(a, b) := x in P a b) | 1.
@@ -139,6 +135,16 @@ Proof. solve_decidable_transparent. Defined.
 Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A.
 Proof. solve_decidable_transparent. Defined.
 
+Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec.
+Global Instance dec_lt_positive : DecidableRel BinPos.Pos.lt.
+Proof. eauto using Decidable_iff_to_impl, Pos.ltb_lt with typeclass_instances. Defined.
+Global Instance dec_le_positive : DecidableRel BinPos.Pos.le.
+Proof. eauto using Decidable_iff_to_impl, Pos.leb_le with typeclass_instances. Defined.
+Global Instance dec_gt_positive : DecidableRel BinPos.Pos.gt.
+Proof. eauto using Decidable_iff_to_flip_impl, Pos.gt_lt_iff with typeclass_instances. Defined.
+Global Instance dec_ge_positive : DecidableRel BinPos.Pos.ge.
+Proof. eauto using Decidable_iff_to_flip_impl, Pos.ge_le_iff with typeclass_instances. Defined.
+
 Lemma dec_of_semidec {P : Prop} (H : option P) (H_complete : H = None -> ~P) : Decidable P.
 Proof. destruct H; [ left; assumption | right; apply H_complete, eq_refl ]. Defined.
 
@@ -169,4 +175,4 @@ Lemma cast_if_eq_refl {T H P} t v : @cast_if_eq T H P t t v = Some v.
 Proof.
   compute; clear; destruct (H t t) as [ [] |e];
     [ reflexivity | destruct (e eq_refl) ].
-Qed.
+Qed.
\ No newline at end of file