The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear Kevin,

  [autorewrite] is indeed a bit crude, namely it only does [repeat rewrite].

You might prefer more control using the [rewrite_strat] tactic which allows

you to control the traversal strategy and will try to apply the rewrite rule to 

subterms as you instruct it. In your example:

  now rewrite_strat (topdown (hints mydb)).

or 

  now rewrite_strat (bottomup (hints mydb)).

complete your proof. Both strategies are fixpoints: 

- for topdown, if the argument tactic succeeds (here (hints mydb) which

  succeeds when it can use one of the rewrite hints), it calls itself recursively 

  and if it fails it recursively calls itself on subterms or stops making no 

  progress if there are no subterms

- for bottomup, it goes to the leaves of the term first.

https://coq.inria.fr/refman/addendum/generalized-rewriting.html#strategies-for-rewriting

Best,

-- Matthieu

On Thu, Jun 7, 2018 at 8:02 PM Kevin Hamlen <hamlen AT utdallas.edu> 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