coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] setoid rewriting

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] setoid rewriting
Date: Sun, 07 Aug 2016 09:26:33 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f52.google.com
Ironport-phdr: 9a23:9wt9UBxn3Hswp7XXCy+O+j09IxM/srCxBDY+r6Qd0ekWIJqq85mqBkHD//Il1AaPBtSDraIUwLOP+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwud7yzSt6Z1p3//tvx0qWbWx9Piju5bOE6BzSNhiKViPMrh5B/IL060BrDrygAUe1XwWR1OQDbxE6ktY/jtKJkpi9Xorcq89NKeaT8ZaUxC7JCXxo8NGVgwcT3qRnCQBbH3XwOX2wL2k5NChTZ5RTSW57triL/8O1n13/JboXNUbkoVGH6vO9QQxjyhXJfOg==

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

[Coq-Club] setoid rewriting, Vadim Zaliva, 08/01/2016
- Re: [Coq-Club] setoid rewriting, Matthieu Sozeau, 08/07/2016
  - [Coq-Club] setoid rewriting, Pierre Courtieu, 08/07/2016
    - Re: [Coq-Club] setoid rewriting, Vadim Zaliva, 08/08/2016
      - Re: [Coq-Club] setoid rewriting, Matthieu Sozeau, 08/09/2016