The Coq mailing list

[julien forest <forest AT ensiie.fr>]

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