The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

It wouldn't surprise me if one can prove that there is no such way.  The [n] argument to [f] lives in [Set], while your [termination] proof lives in [Prop], and information is not supposed to be able to flow out of proofs into regular program execution!  Clearly the [n] argument has computational significance here; it isn't just an artifact of termination proof like in Coq's well-founded recursion.

On 04/25/2014 11:49 AM, Kirill Taran wrote:

Hello,

I have a fixpoint with "fuel" argument (i.e. argument which restricts depth of recursion).
Then I have a proof that for any argument of this fixpoint there is such "fuel" value, that
the fixpoint suceeds.

Fixpoint f (x : X) (n : nat) : option Y := ...
Lemma termination : forall x, exists n y, f x n = Some y.

But then I somehow can't invent a way to compose then into "good" fixpoint:

Fixpoint f' (x : X) : Y.

Could anybody prompt me how to incorporate the proof into "good" fixpoint?

Sincerely,
Kirill Taran