The Coq mailing list

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

Didn't know about ConstructiveEpsilon module. Thanks for example.
But why will your example not compute? I don't see any axiom usage there.

>  if you just wanted to define it or if you also wanted to use it for computing
It is better to have computable version. I see that Acc is from Wf module but didn't learn it yet,
so it would be good if you could give details.

Sincerely,
Kirill Taran

On Fri, Apr 25, 2014 at 9:22 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

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