The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Pierre and Matthieu, thanks for the responses!

I did not expect the results to be equivalent but I wanted to illustrate that all Foo's instances in the goal are rewritable, at least in this order. 

Perhaps the better example is:  

setoid_rewrite Foo at 1.

vs.

setoid_rewrite Foo.

Shouldn't the following 2 be equivalent?

Vadim

 

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

On Sun, Aug 7, 2016 at 7:50 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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