The Coq mailing list

[jean-francois.monin AT imag.fr]

If you observe that the world is grey, it does not necessarily
mean that the real world is grey. May be you just wear sun glasses.

Even if CIC satisfies an extensional model (I'm not a specialist,
but my guess is that it is the case at least in predicative fragments,
better answers welcome!),
it also satisfies at least one model where quicksort <> bubblesort
(roughly, Coq and friends kernels). 

Proving that 2 functions are (intensionnally) equal is more demanding
than in the usual set-theoretic setting. 
(A non trivial case is:
vanilla sprintf = Danvy's purely functional sprintf).

In many cases, you just live with explicit extensional equality,
replacing only applications (f x) with (g x). Consider also
setoids (and setoid replace).

Regards,
  Jean-Francois Monin

Stefan Karrmann a ecrit :
 > 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