coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] getting rid of fix

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] getting rid of fix
Date: Fri, 11 Sep 2015 00:53:53 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:YQXvGxbqQyW416pwH2UnZB3/LSx+4OfEezUN459isYplN5qZpcm7bnLW6fgltlLVR4KTs6sC0LqK9fm/EjZYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7z0osKYOV0ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JaGIcmBdSH0Dm9hzwVJrrqWOus+N83CicMsn3VqwvcS6l5a1mUgPrkioNPTMj6yfRjpoj3+pgvBu9qkknkMbva4aPOa8mcw==

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.

On 09/11/2015 12:44 AM, Vadim Zaliva wrote:

I have a fixpoint definition which at some point unwrapped to something like
this:

fix z (x:A) := …

after some rewriting of the body it is no longer recursive. How can I get rid
of ‘fix'
and perhaps turn it into regular lambda?

Thanks!

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