The Coq mailing list

[Bas Spitters <b.spitters AT cs.ru.nl>]

Dear Herman,

On Friday 22 April 2005 13:24, herman geuvers wrote:
> I noticed that Coq's unification sometimes introduces too many
> abstractions, causing the apply tactic to take the "wrong branch",
> leading to proof failure.
>
> Here is an example, part of my exercise file for students where they
> prove an instance of the Knaster-Tarski fixed-point theorem.
>
> Did anyone else ever come accross this?
> Is this a failure of Coq's unification?

It seems that this is correct. Coq seems to choose the eta-expansion: (fun 
x0 : A => P x0) in the most general unifier.

Your problem is not caused by *intensionality*, but by the lack of  
eta-conversion!
Alexandre Miquel claims:
http://pauillac.inria.fr/pipermail/coq-club/2004/001435.html
> Coming back to the problem of eta-conversion, the situation is
> actually completely different, since 1. this axiom is refuted by
> no natural counter-model construction, and 2. there is - as far as
> I know - no serious philosophico-technical arguments against eta.
> Moreover, the eta-conversion rule could be even incorporated at the
> level of Coq's conversion test machinery (by performing eta-expansions
> on the fly), thus removing the need for an extra axiom.
> 
> I personally think that the system would really benefit from this,
> at least because 1. the system would be easier to understand, and
> 2. unification becomes much simpler in presence of eta-conversion.
> 
> So an interesting question is: why is eta-conversion still not
> considered in Coq's conversion test?  Hmm... I think that this
> situation is due to historical reasons.  Only.    :-)

I tend to agree with him. So let me repeat his question:
why is eta-conversion still not considered in Coq's conversion test?

Bas

-------------------------------------------------------
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/
P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
spitters AT cs.ru.nl
 Ph:+31-24-3652631 F:+31-24-3652525 Room: A5024