The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Feb 01, 2007 at 09:55:48PM +0100, Eric Jaeger wrote:

> Is this result provable in Coq without additional axiom ?

> Theorem f_abst:forall (dom ran:Set)(P:(dom->ran)->Prop)(f:dom->ran),
> P f->P (fun (d:dom)=>f d).

> I mean, f and (fun (d:dom)=>f d) are more than extensionnally
> equal...

Yes, they are eta-convertible. The conversion from one to the other is
called "eta conversion". As far as I remember, eta conversion is not
part of the Coq baked-in convertibility, but adding it as an axiom
does not break consistency.

Recent discussion on that issue on this mailing list:

 http://pauillac.inria.fr/pipermail/coq-club/2006/002514.html
 http://pauillac.inria.fr/pipermail/coq-club/2006/002515.html

-- 
Lionel