The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/13/2015 09:58 AM, Jonathan Leivent wrote:
> On 11/13/2015 05:33 AM, Pierre-Marie Pédrot wrote:
> > On 13/11/2015 05:41, Jonathan Leivent wrote:
> > > I compared a problematic rewrite in *|- against a
> > > repeat/match/context/rewrite tactic that does the same set of rewrites
> > > in the goal, and the rewrite in *|- was 8X slower.  But, removing the
> > > context pattern removes the 8X speedup.
> > Probably due to the cost of finding paths through setoid_rewrite. Do you
> > have a reproducible and minimal example?
>
> It will take me a while to prepare something small.  Maybe Jason's 
> coq-bug-finder can be used to assist this process.  I'll work on it...

I tried the easiest thing first - simply factor out the particular 
subgoal I used in this test into a standalone "Goal".  Quite 
surprisingly, that didn't work - the "rewrite in *|-" went very fast in 
that standalone goal.

I then went back into the original proof and admitted all prior subgoals 
that did rewrites before the subgoal I tested, so that the tested 
subgoal would be the first with rewrites - and again the "rewrite in 
*|-" in that tested subgoal were very fast.

I then used abstract on those prior subgoals, instead of admits, so that 
the full subgoal proofs with rewrites would go through, but wouldn't 
appear in the proof term.  That again made the slowdown disappear in the 
tested subgoal!  In fact, the time went down to 0.1 secs.

So, "rewrite in |-*" is carrying around some burden from prior subgoals 
in the same proof.  Perhaps it is performing the search on the entire 
proof term up to that point (which is large if I don't do those admits 
or abstracts), instead of just on the particular subgoal's context?

-- Jonathan