The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 08.11.2012 21:01, schrieb AUGER Cédric:
> 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!)

The basic idea is that you want to differentiate whether you talk about 
procedures or about functions. As Cédric pointed out, just because two 
procedures compute the same result, that doesn't mean they are equal. 
Obviously, every procedure represents a function. We can pretend that we 
argue about the functions and not about the procedures, but it has been 
said before that this is a dangerous thing to do: procedures can be 
applied and the outcome can be computed. Is the same true for functions? 
I don't know.

One thing that has opened my eyes a little bit was this provable 
proposition that Smolka and CE Brown showed to me:

Goal forall X, forall f : X -> (X -> Prop),  exists g, forall x, f x <> g.

What does this mean? Does it mean that there are more "sets of X" than 
there are "elements of X"? Or does it just mean that there is no 
procedure (in the Coq-World) that gives every procedure in (X -> Prop) a 
unique object of X? Certainly you can only write down countably many 
procedures (or "sets") in Coq, but the number of sets of e.g. natural 
numbers is much larger.

Kind regards, Jonas