The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

> Is there a technical reason why there is no extensional equality 
> principle for function types?  The base library has surjective pairing 
> for products, but nothing like this axiom:
> 
> Axiom extensionality : forall (A:Set) (B:Set) (f:A->B)(g:A ->B),
>   (forall x:A, f x = g x) -> f = g.
> 
> Connor McBride's recent post (in the thread "Cannot Rewrite Under 
> Lambda") indicates that it is not possible to prove this as a lemma, but 
> does adding this axiom lead to inconsistencies?

This question comes up often, but is actually answered (in the
negative) in the Coq FAQ, http://coq.inria.fr/doc/faq.html, question
31, which contains an interesting list of "safe" axioms and their
relative strengths.

Speaking of extensionality and the FAQ, I find the answer to question
35 rather dubious (although it conforms to the party line):

« Extensionality of functions is an axiom in, say set theory, but from
  a programing point of view, extensionality cannot be a priori accepted
  since it would identify, say programs such as mergesort and
  quicksort. »

Coq's conversion rules already identify some rather different programs
such as the following linear-time and exponential-time algorithms:

  Fixpoint two_to_the (n: nat) : Z :=
    match n with O => 1 | S m => let r := two_to_the m in r + r end.

  Fixpoint two_to_the' (n: nat) : Z :=
    match n with O => 1 | S m => two_to_the' m + two_to_the' m end.

So, I don't quite see why functional extensionality "cannot be
accepted from a programming point of view", but the above
identification can...

- Xavier Leroy