The Coq mailing list

[Stefan Karrmann <S.Karrmann AT web.de>]

roconnor AT theorem.ca
 (Mon, Aug 07, 2006 at 03:32:14AM -0400):
> On Mon, 7 Aug 2006, Fabrice Lemercier wrote:
> >>You cannot. Eta allows you to identify very similar
> >>functions but not,
> >>say, quicksort and bubble sort.

How do we get in Coq a difference between quicksort and bubble sort?
We cannot observe the runtime of these functions. (Neither the number of
reductions, matches or applies.)

In Coq you can only compare the values of the applied functions. - These
are equal, i.e. forall x. quicksort x = bubble_sort x.

> >What about the following argument taken from
> >Wikipedia?
> >
> >if  f a==g a  for all lambda expressions a, then in
> >particular by taking a to be a variable x not
> >appearing free in f nor g we have  f x == g x  and
i.e. forall x. (f x == g x)
> >hence  ? x. f x == ? x. g x,  and so by eta-conversion
> >f == g.

Regards,
-- 
Stefan Karrmann

I didn't get sophisticated -- I just got tired.  But maybe that's what
sophisticated is -- being tired.
                -- Rita Gain