The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Thu, 11 Oct 2007 17:20:18 +0100, Edsko de Vries 
<devriese AT cs.tcd.ie>
a écrit:
> > Function foo (l: L) : nat := match l with
> >   | Base => 0
> >   | Ind l' => match l' with
> >     | Base => 0
> >     | Ind l'' => foo l''
> >     end
> >   end. 
> > (* See the message for a list of things defined here. For example Check 
> > foo_ind *)  
> 
> I'm not sure what message you are referring to here? After the Inductive
> L.. definition, I get "L is defined; L_rect is defined; L_ind is
> defined; L_rec is defined" but after the Function foo.. definition, I
> get no messages at all (I'm using coqide, Coq version 8.1pl1).

OK coqide probably hides such messages.

Here are them:

foo is recursively defined (decreasing on 1st argument)
foo_equation is defined
foo_ind is defined
foo_rec is defined
foo_rect is defined
R_foo_correct is defined
R_foo_complete is defined

Interesting things are foo_equation, which is the fixpoint equation of
foo, and the 3 induction principles foo_ind foo_rec foo_rect that
correspond to the recursive structure of foo and are used by functional
induction.



> > Theorem foo_zero : forall (l:L), foo l = 0.
> > Proof.
> >   intros l.
> >   functional induction (foo l). (* this makes actually use of foo_ind, 
> > automatically built by Function *)
> >   reflexivity.
> >   reflexivity.
> >   assumption.
> > Qed.  
> 
> Well that was easy! Very nice. I'm not sure how it works though; what
> should I read to understand "Function" and "functional induction"?

Documentation section 2.3, online is maybe not completely up to date.
The best is to compile trunk version of the doc (maybe).

Cheers,
P.