The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le ven. 8 juin 2018 à 08:08, Kevin Hamlen <hamlen AT utdallas.edu> a écrit :

Dear Matthieu,

Thank you for the pointer!  I didn't know about "rewrite_strat".  It indeed appears to be very powerful.

But it also seems to be strangely slow, and I'm not sure I understand why.  Running "rewrite_strat (topdown (hints mydb))" on a large term takes much longer to complete than my Ltac, which just context-matches on all the patterns of hints in the database and tries all the matching lemmas on each.  Here's a minimal example:

Require Import NArith.
Open Scope N.

Hint Rewrite N.mod_small using assumption : mydb.

Definition large_term (m:N) (x:N): N.
  do 300 refine (_ mod m). exact x.
Defined.

Ltac my_rewrite :=
  repeat match goal with [ |- context [ ?x mod ?y ] ] => rewrite (N.mod_small x y) by assumption end.

Goal forall x y m, x < y -> large_term m (x mod y) = large_term m x.
  intros. unfold large_term.
  assert_succeeds (time my_rewrite). (* takes about 10s on my machine *)
  time rewrite_strat (topdown (hints mydb)).  (* takes about 50s on my machine *)
  reflexivity.
Qed.

Here I get a 5x performance hit using rewrite_strat with topdown vs. my manual approach, and with a larger hint database I get as much as 1000x slow-down.  So something obviously isn't scaling well.  But isn't my Ltac essentially doing exactly what topdown does?  Perhaps I don't yet understand how rewrite strategies work.

Hi Kevin,

  It might be the unification strategy used by rewrite_strat which differs and takes much longer to fail than the syntactic matching you perform here. You might want to guard the rewrite with a `pattern` strategy that does syntactic matching as your Ltac code does. Also, contrary to rewrite, rewrite_strat does not treat the equality type specially and uses generalized rewriting to produce the proof of the toplevel equality, whereby a proof-search is performed which might slow things down.

Cheers,

— Matthieu

On 6/7/2018 1:27 PM, Matthieu Sozeau wrote:

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