coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vadim Zaliva <vzaliva AT cmu.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] more naive questions about rewriting
- Date: Wed, 17 Aug 2016 16:16:30 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
- Ironport-phdr: 9a23:Rx1LJRRXilZGYeayMbk+6mOqHNpsv+yvbD5Q0YIujvd0So/mwa64Yh2N2/xhgRfzUJnB7Loc0qyN4vmmAzdLuMjJ8ChbNscdD1ld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbshsi6n9q/54fUK10RwmHsOPUod17v802R7pBQ2to6bP5pi1PgmThhQ6xu32RmJFaezV7Xx/yb29pdyRlWoO8r7MVaUK/3LOwSRL1cCyk6YShuvJW4/S/4UBCX63AAfmITmxtOS0iZvVCpFqv25yD9r6923DSQFczwV7E9Hzq4vIlxTxq9ti4LNjtxwmjTi9J5xPZFshulpgJ264XRfceYOOcoLfCVRs8TWWcUBpUZbCdGGI7pM9oC
On Wed, Aug 17, 2016 at 12:29 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:
I'm not sure why you would need to specify a relation for setoid_rewrite, as it is always inferred from the lemma itself. Do you have an example?
I just have a situation where:
replace a with b by apply compose_assoc.
works instantly
while
setoid_rewrite <- compose_assoc at 9.
takes forever. I haven not been able to see if it finishes. Here is a log
file for first few minutes:
expressions 'a' and 'b' are approximately 400 lines long each. Even if I use (set with wildcards trick proposed by Laurent, I do not have to spell out 'a' but I still need manually construct and write down 'b'. So making 'setoid_rewrite ... at n' could really help here.
My initial theory was that it was using wrong relation for rewriting and tries and fails to find all Proper instances required for such rewrite. But apparently it is something else.
--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
- [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/16/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/16/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, John Wiegley, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Jonathan Leivent, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/19/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
- Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/16/2016
Archive powered by MHonArc 2.6.18.