Gaëtan Gilbert (Nov 30 2021 at 10:24): Gaëtan Gilbert (Nov 30 2021 at 10:24):I'm looking for examples of how to use rewrite_strat to test changes in its code and generally to try to understand it more
Examples of various complexities and runtimes are welcome, but preferably without dependencies outside the stdlib
particularly nice examples may end up in the test suite and/or the refman
Jason Gross (Nov 30 2021 at 16:46):If I recall correctly, there's a couple of uses in coq-community/coq-performance-tests. They're currently geared at automated performance testing rather than readability
Jason Gross (Nov 30 2021 at 16:53):https://github.com/coq-community/coq-performance-tests/blob/master/src/fiat_crypto_via_setoid_rewrite_standalone.v is probably the best example I've seen of the limitations of rewrite_strat (the worst one being that there's no NbE-order for rewriting, only topdown and bottomup, and the second-worst one being that it generates invalid proof terms if you sequence rewriting and reduction in the wrong order)
Jason Gross (Nov 30 2021 at 16:54):(note that this example is also real-world-scale; much of the work of fiat-crypto would not be needed if rewrite_strat handled this example adequately)
Gaëtan Gilbert (Dec 07 2021 at 13:36):if there wasn't https://github.com/coq/coq/issues/10934 what would the rewrite strat tactic look like? just https://github.com/coq-community/coq-performance-tests/blob/d17f35704661588dcd6ecc13a2bdca990fb68bd8/src/fiat_crypto_via_setoid_rewrite_standalone.v#L517-L520 ?
Gaëtan Gilbert (Dec 16 2021 at 15:26):@Jason Gross ping
Gaëtan Gilbert (Dec 16 2021 at 15:50):@Matthieu Sozeau do you have any examples?
Jason Gross (Dec 16 2021 at 16:11):https://github.com/coq/coq/issues/10923 is a much more pressing issue
Jason Gross (Dec 16 2021 at 16:17):There's a couple more eval cbvs that would need to be merged, but, yeah, the invocation would be much shorter
Gaëtan Gilbert (Dec 16 2021 at 16:22):I'm more trying to understand the example than trying to fix issues for now
Gaëtan Gilbert (Dec 16 2021 at 16:38):although you already debugged this one so may as well try https://github.com/coq/coq/pull/15377
Matthieu Sozeau (Dec 17 2021 at 09:24):@Gaëtan Gilbert I don't have examples no. But basically any autorewrite example could be turned into a rewrite_strat example and should work mostly the same way (I guess using topdown to best emulate the autorewrite strategy)
Last updated: Oct 05 2023 at 02:01 UTC