Reorder Z.euclidean_division_equations_cleanup
#18818
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
added
kind: fix
coqbot-app
bot
added
the
needs: full CI
|
@coqbot bench |
|
Got more than one checkSuite. |
Fixes coq#18770 We first destruct, then clear, then specialize. The reasoning is: - `destruct` before `clear` because the `clear` is not going to make much of a difference to `destruct`, but the `destruct` might expose more opportunities for `clear`ing - `clear` between `destruct` and `specialize` so that we don't waste a bunch of time modifying the goal (via `specialize`) on hypotheses that we would anyway want to `clear`
|
@coqbot bench |
1 similar comment
|
@coqbot bench |
|
🏁 Bench results: 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 94.1990 95.5150 1.3160 1.40% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 254.7720 255.8970 1.1250 0.44% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 16.9140 17.5100 0.5960 3.52% 607 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 0.9320 1.4430 0.5110 54.83% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 63.1260 63.5550 0.4290 0.68% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 81.8340 82.2310 0.3970 0.49% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 24.3530 24.7290 0.3760 1.54% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 4.7850 5.1590 0.3740 7.82% 1258 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 41.7960 42.1660 0.3700 0.89% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 17.5660 17.9310 0.3650 2.08% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 33.8170 34.1430 0.3260 0.96% 1333 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 10.2480 10.5550 0.3070 3.00% 279 coq-category-theory/Theory/Metacategory.v.html │ │ 0.7860 1.0570 0.2710 34.48% 816 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.8380 1.0910 0.2530 30.19% 384 coq-stdlib/MSets/MSetAVL.v.html │ │ 0.0060 0.2380 0.2320 3866.67% 522 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v.html │ │ 0.0390 0.2680 0.2290 587.18% 376 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v.html │ │ 27.6390 27.8680 0.2290 0.83% 1933 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v.html │ │ 10.5960 10.8060 0.2100 1.98% 186 coq-unimath/UniMath/AlgebraicTheories/RepresentationTheorem.v.html │ │ 97.6890 97.8980 0.2090 0.21% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 8.5330 8.7410 0.2080 2.44% 35 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.v.html │ │ 10.2830 10.4870 0.2040 1.98% 496 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 1.9960 2.1920 0.1960 9.82% 1088 coq-category-theory/Functor/Construction/Product/Monoidal.v.html │ │ 78.9440 79.1380 0.1940 0.25% 365 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 11.5560 11.7480 0.1920 1.66% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 46.3510 46.5370 0.1860 0.40% 915 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 35.1060 1.0330 -34.0730 -97.06% 21 coq-performance-tests-lite/src/zify_large_context.v.html │ │ 4.6800 0.2570 -4.4230 -94.51% 17 coq-performance-tests-lite/src/zify_large_context.v.html │ │ 75.5430 73.4100 -2.1330 -2.82% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 1.5890 0.6150 -0.9740 -61.30% 1080 coq-bedrock2/bedrock2/src/bedrock2/unzify.v.html │ │ 1.5860 0.6180 -0.9680 -61.03% 1080 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2/unzify.v.html │ │ 44.6920 43.8870 -0.8050 -1.80% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 2.4290 1.7910 -0.6380 -26.27% 736 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 1.6090 1.0470 -0.5620 -34.93% 323 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.v.html │ │ 1.6080 1.0500 -0.5580 -34.70% 323 coq-bedrock2/bedrock2/src/bedrock2Examples/memmove.v.html │ │ 12.2610 11.7220 -0.5390 -4.40% 827 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 2.7450 2.2210 -0.5240 -19.09% 481 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.8230 2.3080 -0.5150 -18.24% 480 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.8180 2.3090 -0.5090 -18.06% 480 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.7250 2.2250 -0.5000 -18.35% 481 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 0.8100 0.3240 -0.4860 -60.00% 102 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/uint128_32.v.html │ │ 1.2240 0.7500 -0.4740 -38.73% 887 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html │ │ 2.5990 2.1290 -0.4700 -18.08% 483 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 0.7960 0.3270 -0.4690 -58.92% 102 coq-bedrock2/bedrock2/src/bedrock2Examples/uint128_32.v.html │ │ 1.2240 0.7560 -0.4680 -38.24% 887 coq-bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html │ │ 2.5670 2.1000 -0.4670 -18.19% 482 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.5670 2.1050 -0.4620 -18.00% 482 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.5960 2.1450 -0.4510 -17.37% 483 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 154.7050 154.2680 -0.4370 -0.28% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 10.0400 9.6090 -0.4310 -4.29% 828 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 9.3320 8.9170 -0.4150 -4.45% 829 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
The
destruct q_nice_strong with (b:=b) (k:=k) (m:=mu) (offset:=1) (a:=x) (n:=M) as [cond Hcond];
eauto using Z.lt_gt with zarith.was not taking 95 seconds when we first wrote that line, and something is going wrong?) Everything else looks good to me. @coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
andres-erbsen
approved these changes
Mar 20, 2024
| | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H | ||
| | [ H : 0 <= ?x < _ |- _ ] => destruct H | ||
| end. | ||
| repeat |
There was a problem hiding this comment.
Is this repeat here because specialize in the old version actually trigger more clear later, whereas in the new version there is no such opportunity without this repeat?
There was a problem hiding this comment.
Not just more clear but also more destruct, yes. I'm not 100% sure that it gets used in practice, but I expect it to be relatively cheap to run the final iteration, and I think it's better to not have to manually track whether or not specialize can reveal more opportunities for clear and destruct
|
@coqbot merge now |
|
@andres-erbsen: You cannot merge this PR because:
|
|
@andres-erbsen I've set a milestone, so this can now be merged |
|
@coqbot merge now |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We first destruct, then clear, then specialize. The reasoning is:
destructbeforeclearbecause theclearis not going to make much of a difference todestruct, but thedestructmight expose more opportunities forclearingclearbetweendestructandspecializeso that we don't waste a bunch of time modifying the goal (viaspecialize) on hypotheses that we would anyway want toclearFixes #18770