The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Kirill,

Expanding on Adam’s response, if you could prove termination as something like this:

Lemma termination : forall x, { n | exists y, f x n = Some y }

then you could use this function to generate the n argument to f. This is because the { n | … } construct is in Set, while exists n, … is in Prop.

If you cannot prove termination in Set but you really need to call f with it, then there are a number of axioms you could use, such as indefinite description (in the library Coq.Logic.IndefiniteDescription), but, because these are axioms, they will get “stuck” and not ever actually produce your “fuel”.

-E

On Apr 25, 2014, at 8:51 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