The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 8 Nov 2012 21:19:43 +0200,
Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 a écrit :

> Hello.
> 
> > Short answer: your lemma is actually _not_provable_ in Coq, but
> > many users assert it as an axiom.  For more details, see Section
> > 10.6 of CPDT <http://adam.chlipala.net/cpdt/>.
> 
>   But there are no explanations about why the functional
> extensionality is not used by default (for "auto" tactic,
> for example; moveover, requires explicit Require Import).
> So, are there any cases when this axiom is undesirable?
> Can it break something?  I'd be glad to know about it (either
> in coq-club or from CPDT).
>   (btw, your book is great!)

I do not really know of any such case, and in fact eta-expansion (a
very particular case of functional extensionality) now belongs to Coq
native logic, and you can prove (λ x, f x = f) now.

But for the general case, I wouldn't be surprised to learn that some
axioms are inconsistant with it. I think I have read here about
univalence type theory where the "eq" type is allowed to have many
inhabitants. I have not read anything on this theory, some I may have
misunderstood, but well, there are cases some people do not want to add
axioms. Plus you need some extra-care to ensure you did not mistyped
your axiom and wrote something different which is not consistant.

Last point, functionnal extensionality is a little strange, since when
you write a function in computer science, you expect it to need some
time to compute when passing arguments. This time is not expressible in
Coq, but in practice, you cannot say that you can use:

let f x = let u = ackermann x x in x+1

each time you have

let f x = x + 1

in an eager language. So, it is seems weird to say these functions are
equal (although it is from a mathematical point of view).

Another thing is that there are many many many axioms we could add to
Coq without breaking consistancy, then we need to choose some arbitrary
subset of them. Adding none seems a good compromise, as you still can
import modules declaring them, or declare your own if you need them.