coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] getting rid of fix

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] getting rid of fix
Date: Thu, 10 Sep 2015 16:11:05 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-pa0-f42.google.com
Ironport-phdr: 9a23:EJnDbRE9Dzz8/IPXXxdaZp1GYnF86YWxBRYc798ds5kLTJ75pM2wAkXT6L1XgUPTWs2DsrQf27aQ6v+rAzFIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6brpNaJPk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4iW2kXl1J6CgzE8hiyConjuy/7qONV0yyHe8D6UOZnCnyZ8653RUqw2288PDkj/TSPhw==

> On Sep 10, 2015, at 15:53 , Robbert Krebbers
> <mailinglists AT robbertkrebbers.nl>
> wrote:
>
> You cannot. At least, not by conversion. A fix only reduces in case it is
> applied to a constructor. You have to "destruct" argument somehow.
>
> You can of course prove an "unfold lemma" to hide this stuff.

Thanks! I noticed that if I destruct on argument the 'fix' is gone. But that
leaves me with several cases to deal with which is inconvenient.

I understand proving “unfold” lemma would involve exact same approach
(destructing argument)?

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva

[Coq-Club] getting rid of fix, Vadim Zaliva, 09/11/2015
- Re: [Coq-Club] getting rid of fix, Robbert Krebbers, 09/11/2015
  - Re: [Coq-Club] getting rid of fix, Vadim Zaliva, 09/11/2015
    - Re: [Coq-Club] getting rid of fix, Gregory Malecha, 09/11/2015