The Coq mailing list

[St�phane Lescuyer <lescuyer AT lri.fr>]

Well, arguably, the most "canonical" example is just fold_left vs.
fold_right on lists. If you need to prove a property on (fold_left f l
i) by induction on the list l, you can use fold_left_rev_right (in the
standard library) to change the fold_left in a fold_right on (rev l),
and then use rev_induction (induction on the reverse of a list).
The advantage of fold_right is that the recursive call has the same
arguments than the current call, so you can use your IH directly
without stating particular invariants on the accumulator.

Incidentally, that's the way the induction principle for finite sets
in FSetProperties was proved (and the reason why it was proved as well
:-) because I was quickly fed up of doing all this manually).

Stéphane L.

2009/3/30 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06