The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 25/04/2014 17:49, 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?


Require Import ConstructiveEpsilon.

Parameter X Y : Type.
Parameter f : X -> nat -> option Y.
Hypothesis termination : forall x, exists n y, f x n = Some y.

Definition f' : X -> Y.
Proof.
intros x.
destruct (constructive_indefinite_ground_description_nat
  (fun n => match f x n with Some _ => True | _ => False end))
  as [n Hn].
- intros n.
  case f.
  intros _.
  now left.
  now right.
- destruct (termination x) as [n [y H]].
  exists n.
  now rewrite H.
- now destruct (f x n) as [|y].
Defined.

This function will not really compute. It was not clear from your email 
if you just wanted to define it or if you also wanted to use it for 
computing. If the latter, there is a standard trick using the Acc 
predicate to get it to compute. I can give more details if needed.

Best regards,

Guillaume