The Coq mailing list

[James McKinna <james.mckinna AT cs.ru.nl>]

Dear Edsko, and others,

a simpler example might be to try to show, for example, commutativity of 
addition on natural numbers defined tail-recursively as

plus 0 n = n
plus (S m) n = plus m (S n)

We discussed this problem (and automatic techniques for solving it, due 
to Andrew Ireland and Alan Bundy in particular) at the Dagstuhl 9350 
meeting in 1995...
   http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=9530

But I can't find Andrew's paper on it out there in TV-land ("Rippling to 
meet the challenge", I think it was called, given during the last 
session on challenge problems). You might check with him directly...

best wishes,

James McKinna



Stéphane Lescuyer wrote:
> 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
> >
> >     
>
>
>
>