The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I would expect such a proof to be metatheoretic, because Coq is believed to be consistent with the axiom [exists x, P x -> { x | P x }].

If you can refine your termination lemma to live in Set rather than Prop, you should be fine; can you prove forall x, { n : nat | exists y, f x n = Some y }?

-Jason

On Apr 25, 2014 11:52 AM, "Adam Chlipala" <adamc AT csail.mit.edu> wrote:

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