The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

AFAIK there is no reason these two tactics should be equivalent. setoid_rewrite only detects possible simultaneous rewriting but does not perform repeat in any way. The repeat can take advantage of the intermediate results to find new redexes.
For instance in the word rewriting context:
Foo: aabb -> ab
On aaabbb
Repeat Foo at 1 gives ab (due to intermediate result aabb).
Whereas setoid only gives aabb. 

That said, it does not explain why setoid_rewrite takes so long. But as a general rule you can not expect thes tactics to behave identically unless particular cases.

P.

On dim. 7 août 2016 at 11:27 Matthieu Sozeau <mattam AT mattam.org> wrote:

It might be due to the compatibility constraints of the first being weaker than the second (which attempts a parallel rewrite of all the instances of Foo in the goal), leading to a divergence in the proof search.
-- Matthieu

On Mon, 1 Aug 2016 at 22:16, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Could anybody please explain to me why the following works:

repeat setoid_rewrite Foo at 1.

while this one does not (takes forever):

setoid_rewrite Foo.

I am using 8.5pl2.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060