optimize Products.v #1938
optimize Products.v #1938
Conversation
Signed-off-by: Ali Caglayan <alizter@gmail.com> <!-- ps-id: 9970e87a-edc2-49b1-9883-fabb57278b1f -->
There was a problem hiding this comment.
Nice. I had noticed that this file was the slowest in the library. Even after this change, it's still a bit slow. This file https://jdc.math.uwo.ca/tmp/Products.html shows the slow lines, in case you want to improve things further. But that can also be done in the future.
| nrapply cat_idl; exact _. | ||
| - intros a b c f g r i. | ||
| apply cat_assoc. | ||
| nrapply cat_assoc; exact _. |
There was a problem hiding this comment.
Are these any different from just using rapply?
There was a problem hiding this comment.
Seems to be faster as rapply uses typeclasses during unification and nrapply doesn't and trivially solves them later.
There was a problem hiding this comment.
When I say seems to be faster, it's the difference between 0.002 and 0.001.
There was a problem hiding this comment.
If it's that small, maybe go with the simpler way? But no big deal either way. And it's fine to merge this and deal with the slow Defined and section End lines later.
| 3: nrapply cat_assoc; exact _. | ||
| 2: refine (_ $@L _). | ||
| 2: apply cat_pr2_fmap01_binprod. | ||
| 2: nrapply cat_pr2_fmap01_binprod; exact _. |
There was a problem hiding this comment.
Same here (and maybe other spots that I missed).
|
@jdchristensen I definitely think there are some better optimizations that could be done. I also inspected the timing htmls and saw that the I just wanted to get these easy optimizations out of the way as I add things to this file in #1929. |
This switches
applytonrapplywhere applicable and a few miscellaneous inlines.See #1937 for the script that times.
Before
After