The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hi,

a while ago there was a similiar question on this list.
Your goal is (almost) the axiom of (functional) extensionality.
In math it is commonly assumed, but in computer science it is not (always)
assumed.

roconnor AT theorem.ca
 (Wed, Feb 02, 2005 at 10:08:58AM -0500):
> Can anyone provide me with a reference that shows that
> 
> forall (T U : Set) (f g : T -> U),
> (forall x : T, f x = g x) -> (fun y : T => f y) = (fun y : T => g y)
> 
> is not provable in Coq?
> 
> Thanks.

Alexandre Miquel (Mon, Sep 20, 2004 at 03:26:36PM +0200):
> > 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

Regards,
-- 
Stefan Karrmann