The Coq mailing list

[jean-francois.monin AT imag.fr]

Hello,

You cannot. Eta allows you to identify very similar functions but not,
say, quicksort and bubble sort.

Sincerely,

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 03 72
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 44 

Fabrice Lemercier a ecrit :
 > Hello,
 > 
 > I can prove in Coq that extensionality implies
 > eta-conversion.
 > How can I prove the  converse?
 > 
 > Lemma ext_eta :
 >   forall  A B:Set,
 >   (forall f1 f2:A->B, (forall x, f1 x = f2 x) -> f1 =
 > f2) ->
 >   (forall f:A->B, (fun x => f x) = f).
 > Proof.
 > intros.
 > apply H.
 > intro.
 > reflexivity.
 > Qed.
 > 
 > Lemma eta_ext :
 >   forall A B:Set,
 >   (forall f:A->B, (fun x => f x) = f) ->
 >   (forall f1 f2:A->B, (forall x, f1 x = f2 x) -> f1 =
 > f2).
 > Proof.
 > ???