The Coq mailing list

[Fabien Renaud <Fabien.Renaud AT inria.fr>]

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!