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

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

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)

(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)

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 ?

@Jason Gross ping

@Matthieu Sozeau do you have any examples?

https://github.com/coq/coq/issues/10923 is a much more pressing issue

There's a couple more eval cbvs that would need to be merged, but, yeah, the invocation would be much shorter

I'm more trying to understand the example than trying to fix issues for now

although you already debugged this one so may as well try https://github.com/coq/coq/pull/15377

@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