coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <mattam AT mattam.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] more naive questions about rewriting
- Date: Wed, 17 Aug 2016 07:29:54 +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-f44.google.com
- Ironport-phdr: 9a23:uR0LSRx8KMFr7mPXCy+O+j09IxM/srCxBDY+r6Qd0e8QIJqq85mqBkHD//Il1AaPBtSCrasUwLOP6OigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJVwYz2PkOvsydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+vh7aCACL+3E0U2MMkxMODRKWwgv9W8LUuzfmtutwxWGhOt/7RK18DTGr87tiTTftgTsbPjt/93vY3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz
Hi Vadim,
On Wed, Aug 17, 2016 at 1:26 AM Vadim Zaliva <vzaliva AT cmu.edu> wrote:
On Tue, Aug 16, 2016 at 3:20 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:[setoid_rewrite <-compose_assoc at 2] works in Vadim's example. The way that setoid_rewrite matches patterns is different from the way that rewrite matches patterns. I think that setoid_rewrite's method is more intuitive.That's very interesting. Thanks! I think it would good to mention this in the documentation. Confusingly it mentions that 'rewrite ... at ..." uses Setoid equality, but apparently that does not mean that it matches patterns in the same way as 'setoid_rewrite'.
Indeed, it's again the difference between n-th occurrence of the first instance of the lemma and n-th occurrence found for any instance of the lemma.
My remaining problem is that I am working in environment where I am already using setoid equality and thus my 'default_relation' is re-defined ('equiv' not 'eq'), while `comp_assoc` is defined for 'eq'. So I need to find a way to use `setoid_rewrite` tactics but with 'eq' relation. You can specify one for 'setoid_replace' tactic ('using relation' argument), but unfortunately not for `setoid_rewrite`!
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?
Best,
-- Matthieu
- [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.