Stream: Coq users

Topic: `rewrite_strat repeat foo` vs `repeat (rewrite_strat foo)`


view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:53):

Is there a clear reasons why the two aren't equivalent? Because it seems like they should be?

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 13:55):

OTOH, since (according to the manual) repeat is equivalent to a strategy using sequencing, that equivalence might suffer from sequencing bugs:
https://github.com/coq/coq/issues/10934

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 14:14):

Oh. For extra fun, that's fixed by going from terms to nested choices:

Time rewrite_strat (repeat (outermost (choice except_0_exist (choice except_0_and except_0_idemp)))).  (* [repeat] works correctly *)
Time rewrite_strat (repeat (outermost (terms except_0_exist except_0_and except_0_idemp))). (* [repeat] doesn't actually work *)

So the last can be successfully rewritten to the sensible strategy topdown:

    Time rewrite_strat (topdown (choice except_0_exist (choice except_0_and except_0_idemp))).

Last updated: Jan 27 2023 at 00:03 UTC