Stream: Coq users

Topic: seeking rewrite_strat examples


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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 ?

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 15:26):

@Jason Gross ping

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 15:50):

@Matthieu Sozeau do you have any examples?

view this post on Zulip Jason Gross (Dec 16 2021 at 16:11):

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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 16:22):

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

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC