The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Actually, I just didn't notice this issue with universes difference.
Suppose, that I can prove termination in Set.

> (Jason) If you can refine your termination lemma to live in Set rather than Prop, you should be fine
> (Eddy) then you could use this function to generate the n argument to f
It is clear, seems that I didn't succeed earlier because just couldn't destruct "exists"
(I tried to defined "good" fixpoint with tactics and Coq gave me error about "exists":
"Case analysis on sort Set is not allowed for inductive definition ex").

Also, I am not sure that { n | exists y, f x n = Some y } is ok for me,
because I need to extract y, but it is inside Prop again.
And I can't construct { n | { y | f x n = Some y } },
because second argument must be in Prop.

Sincerely,
Kirill Taran

On Fri, Apr 25, 2014 at 8:03 PM, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

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