The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Thanks for the quick reply!

> Indeed standard induction scheme are relatively weak compared to more
> general ones like well founded induction (see theories/Wellfounded/*.v).

Yes, but the generality of the wellfounded stuff is more than I need (I
just need an extra 'deeper' recursive call), and as you say, that makes
it more difficult.

> However they are easier to use. I suggest you use the new "Function"
> feature instead of Fixpoint. It gives you among other things a useful
> (but still in the style of L_ind) induction scheme from the function
> definition.
> 
> 
> Inductive L : Set := 
>   | Base : L
>   | Ind : L -> L.
> 
> 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).

> 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"?

Thanks, as always much appreciated!

Edsko