The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

"rewrite ... by tac" and autorewrite with hints of the form "... using tac"
do not backtrack to other matching occurrences if "tac" fails.
I think this is very unfortunate, but apparently that's the intended
behavior.
To get backtracking, there's an undocumented "rewrite*" and "autorewrite*",
but it seems that "autorewrite*" does not work:
https://github.com/coq/coq/issues/7672


On Thu, 2018-06-07 at 13:02 -0500, Kevin Hamlen wrote:
> Dear Coq users,
> 
> I'm finding that "autorewrite" fails to consider rewriting opportunities 
> within patterns that match a hint but fail it.  Is this behavior 
> intentional?  Here's an example:
> 
> Require Import NArith.
> Open Scope N.
> 
> Hint Rewrite N.mod_small using assumption : mydb.
> 
> Goal forall x y z, x < y -> (x mod y) mod z = x mod z.
>    intros.
>    Fail progress (autorewrite with mydb).
>    (* This unfortunately fails to progress even though it could 
> successfully rewrite "x mod y" to "x".  It fails because it first tries 
> rewriting "(x mod y) mod z" to "x mod y" and is unsuccessful, and then 
> never looks for rewrite opportunities within the matched pattern. *)
> 
>    (* If I manually strip the "_ mod z" part, it finds the pattern and 
> rewrites it: *)
>    apply (f_equal (fun n => n mod z)).
>    progress (autorewrite with mydb).
>    reflexivity.
> Qed.
> 
> Is there any work-around?  This behavior unfortunately makes autorewrite 
> useless for most of my patterns, forcing me to resort to much slower Ltacs.
> 
> Cheers,
> Kevin
> 
>