The Coq mailing list

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

Hi,

On 30 Mar 2009, at 13:21, Stéphane Lescuyer wrote:

> To rebound on Julien's reply, just a more general remark : it is
> almost always harder to reason about tail-recursive functions because
> you need to manually introduce the adequate invariant on the
> accumulator  (in that case, the function F) in your induction
> principles.
>
> For instance, to prove your lemma, you could have proven the following
> (more general) result by induction on n, by adding a property on F :
> Lemma for_aa : forall (n nf : nat) (F : nat -> Set),
>  (forall m, m < nf -> F m = unit) ->
>  forall m, m <= n+nf -> iterated_unit_ext F n m = unit.
>
> A good way to proceed is Julien's : start by writing a lemma showing
> that your function is equal to the non tail-recursive version you
> could have written. Then use this lemma to rewrite instead of using
> conversion.
> I just wanted to emphasize that you can use Julien's solution in many
> cases since it is more general that it may look.

That is very interesting, thanks for that remark. Are you aware of  
other examples of this that I could look up?

Edsko