The Coq mailing list

[Alexandre Miquel <Alexandre.Miquel AT pps.jussieu.fr>]

> Hello,
>
> Coq's reference manual mentions eta-conversion only briefly, c.f.
> chapter 4.3 of it. Is the
>
>    Theorem eta_conversion :
>      forall (A:Type) (B:A->Type) (f:forall x:A,B x),
>      (fun x:A=>f x) = f.
>
> provable in Coq without additional axioms?

No, it is not (or seems to be not?) provable without additional
axioms. However, giving a counter-model is difficult, since most
models of type theory (if not all) naturally validate this equality.
(I have some ideas to build a counter-model, but only by using very
artificial constructions...)

> A little bit more general is:
>
> Theorem app_eq :
>    forall (A:Type) (B:A->Type) (f g:forall x:A,B x),
>    (forall x:A=>f x=g x) -> f = g.
>
> If this is provable, then eta_conversion is easy to prove:
> [...]

The statement you are referring to as "app_eq" is known in type theory
as the "axiom of (functional) extensionality".  (Here, it is wiser to
add "functional", since there is also an axiom of "propositional"
extensionality - see Logic/ClassicalFacts in Coq's stdlib.)

As you mention it, the axiom of functional extensionality implies the
eta-equality, but it is actually much stronger.

Unlike the eta-rule, this axiom is refuted by some (interesting)
models of type theory.  You can find such a model in my PhD thesis
(unfortunately written in french) chapter 5, p. 191.

Intuitively, this is easy to understand: No computer scientist would
like to identify quick sort with bubble sort!  (Would you ?)  On the
other hand, both algorithms produce the same output for the same
input, so that the corresponding programs are extensionally equal,
and even *equal* by the axiom of functional extensionality.

Taking the axiom of extensionality - or not - depends on which
equality you want for your system:

* Either you want the equality of computer scientists - that merely
  consider functions as algorithms - and forget about the axiom of
  functional extensionality...

* Either you want the equality of (classical) mathematicians - that
  merely treat functions as infinite hash tables - and consider that
  the axiom of extensionality is very natural.

Both choices are perfectly legitimate - but simply remember that they
don't give you the same equality!

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.    :-)

Regards,

-- Alexandre Miquel