coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] more naive questions about rewriting

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:56:31 -0700
Authentication-results: mail3-smtp-sop.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-f46.google.com
Ironport-phdr: 9a23:z/m2xhyRX3hfSxHXCy+O+j09IxM/srCxBDY+r6Qd0e4fIJqq85mqBkHD//Il1AaPBtSCragfwLCH++C4ACpbsM7H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpqsSVOV4D3mv1Iesrak7n9UOJ7oheqLAhA5558gHOrHpMdrYe7kJTDnXXoSzB4Nyt9oVo6SVatqFp3cdBVaLnY/ZwFuQAX3x1e1wyscbsrFzISRaFznoaSGQf1BRSUCbf6xSvYJ79sy6yhON52TeTdZnoX7kwWCqrx6xuVVnlhDpRZG1xy33elsEl1PETmxmmvREqm4M=

On Wed, Aug 17, 2016 at 4:16 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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.

Found another workaround which allows to avoid spelling full expressions:

remember (compose (foo _ ) _) as c1 eqn: Hc1.

setoid_rewrite <- compose_assoc in Hc1.

subst c1.

but it is still hacky...

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