The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Julien is right:

> You probably have saved your obligation proof by Qed. Try to end it
> with Defined instead.

That was the problem.  Perhaps the Reference Manual could mention this.

Thanks.
Randy
--
On Mon, Apr 25, 2011 at 5:50 AM, julien forest 
<forest AT ensiie.fr>
 wrote:
> Hi Randy,
>
>
> On Sun, 24 Apr 2011 12:10:01 -0400
> Randy Pollack 
>Â <rpollack AT seas.harvard.edu>
>  wrote:
>
>> I tried the "Function" command for the first time, with a simple
>> nat-valued measure.
>>
>> Function psub (P:bbS) (X:PP) (M:bbS) {measure bbS_size M} : bbS :=
>>   match M with
>>     | par Y => (if PPeq Y X then P else M)
>>     | var _ => M
>>     | app Q N => app (psub P X Q) (psub P X N)
>>     | lam n N => lam n (psub P X (rename n X N))
>>   end.
>>
>> (The point is that [bbS_size (rename n X N)] is the same as [bbS_size
>> N].)
>>
>> I proved the generated goals without any problem (using "omega").
>>
>> I want psub to evaluate by computation as if I had defined it by
>> Fixpoint, but this doesn't seem to work; blocked by "psub_terminate".
>
> You probably have saved your obligation proof by Qed. Try to end it
> with Defined instead.
>
>> By playing around, I found that "psub_F psub" evaluates, but how can I
>> use this?
>>
>> I guess there are also propositional equations proved somewhere; is
>> that how the defined function psub is intended to be used?
>
> Indeed, Function generates psub_F (the functionnal of psub),
> psub_terminate (its proof obligations), psub itself, psub_equation (an
> equation lemma), three induction lemma (one for each sort) and two
> lemmas allowing you to use functional inversion.
>
> Best regards,
> Julien Forest
>
>