The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

Foo_func is the functional corresponding to Foo, when defining Foo by
well-founded recursion. Foo is then just the application of the wf recursion
principle to the functional and the proof of well-roundedness.
I'd recommend proving an unfolding lemma after you've defined [test].
It is provided by Function (test_eqn is the name I think), you can run
[Inspect 10] after defining test with Function to see what were the last
definitions.
Actually you'll also need to use measure induction again to prove your lemma.
Function provides a functional elimination principle for each function that 
will use it internally. Just doing functional elimination will do both the
unfolding/case-analysis and provide you with the right induction hypotheses.

Hope this helps,
-- Matthieu

On 2 oct. 2013, at 11:39, Fabien Renaud 
<Fabien.Renaud AT inria.fr>
 wrote:

> Hi,
> 
> I have questions related to Program.
> 
> 
> I simplified my problem to the following:
> 
> Require Coq.Program.Wf.
> 
> Program Fixpoint test (l: list nat) {measure (length l)} :=
> match l with
> | nil => 0
> | X::R => (test (tl R))
> end.
> Obligation 1.
> induction R; simpl; omega.
> Defined.
> 
> Ok my function is defined but now suppose I want to prove this:
> Lemma foo : forall l x, test (x::l) = 0.
> Proof.
> intros.
> 
> Now simpl does nothing, and compute gives me something I don't want to read.
> 
> Is there a way to do this kind of thing with Program? I tried with Function 
> but simpl only expands to function_terminate and I'm stuck.
> 
> By the way, when I defined a Program foo, sometimes I have "foo is 
> defined", and sometimes "foo_func is defined". What does this mean?
> 
> Thanks!