coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] getting rid of fix

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] getting rid of fix
Date: Thu, 10 Sep 2015 22:16:18 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f180.google.com
Ironport-phdr: 9a23:nVOq+RLonN3aB/7fotmcpTZWNBhigK39O0sv0rFitYgULPjxwZ3uMQTl6Ol3ixeRBMOAu64C0raempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRsiL04ye7KObxd76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtLYqySlbuuog+shcSu26Ov1gFf0LRAghZksy/YXAsQTJBV+E4WJZWWELmDJJBRLE5Vf0RMGinDH9s79SwiSVOtfnBZU9XTmp764jHBDtgSMKPD4w2G7Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZfHDIZUw==

Yes, proving an unfolding lemma requires a destruct.

On Thu, Sep 10, 2015 at 4:11 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

> 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

gregory malecha

[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