Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] external proof of termination

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] external proof of termination


Chronological Thread 
  • From: Kirill Taran <kirill.t256 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] external proof of termination
  • Date: Fri, 25 Apr 2014 21:45:59 +0400

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




Archive powered by MHonArc 2.6.18.

Top of Page