The Coq mailing list

[gallais <guillaume.allais AT strath.ac.uk>]

Arg, I did not see Guillaume's answer. Sorry about the noise.

On 28/04/14 11:36, gallais wrote:
> Actually it's pretty simple to build a constructive proof of
> termination using a constructive Epsilon. And then, we can
> just run f using the n we're handed over by the constructive
> proof.
>
> http://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html
>
>
> --------------------------------------------------------------
>
> Require Import Coq.Logic.ConstructiveEpsilon.
>
> Variable (X Y : Set).
> Axiom f : forall (x : X) (n : nat), option Y.
> Axiom termination : forall x, exists n y, f x n = Some y.
>
> Lemma constructive_termination :
>    forall x, { n | exists y, f x n = Some y }.
> Proof.
> intros x ; apply constructive_indefinite_ground_description_nat.
>   intro n ; case (f x n) as [y|].
>    left ; exists y ; reflexivity.
>    right ; intros [y ih] ; inversion ih.
>   apply termination.
> Qed.
>
> Definition run_f (x : X) : Y.
>   destruct (constructive_termination x) as [n proof].
>   case_eq (f x n).
>    intros y _ ; exact y.
>    intros contradiction ; apply False_rec.
>      destruct proof as [y arg].
>      rewrite arg in contradiction ; inversion contradiction.
> Qed.
>
> On 25/04/14 16:51, Adam Chlipala 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