coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
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
Kirill Taran
On Fri, Apr 25, 2014 at 9:22 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:
Require Import ConstructiveEpsilon.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?
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
- Re: [Coq-Club] external proof of termination, (continued)
- Re: [Coq-Club] external proof of termination, Adam Chlipala, 04/25/2014
- Re: [Coq-Club] external proof of termination, Jason Gross, 04/25/2014
- Re: [Coq-Club] external proof of termination, Arnaud Spiwack, 04/28/2014
- Re: [Coq-Club] external proof of termination, Eddy Westbrook, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Eddy Westbrook, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Eddy Westbrook, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, gallais, 04/28/2014
- Re: [Coq-Club] external proof of termination, gallais, 04/28/2014
- Re: [Coq-Club] external proof of termination, Jason Gross, 04/25/2014
- Re: [Coq-Club] external proof of termination, Guillaume Melquiond, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Adam Chlipala, 04/25/2014
- Re: [Coq-Club] external proof of termination, Guillaume Melquiond, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/26/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Adam Chlipala, 04/25/2014
Archive powered by MHonArc 2.6.18.