The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

        Bonjour Henri,


> Ca doit sans doute etre tres simple, mais je ne vois pas comment
> montrer l'axiome d'extensionnalite pour les fonctions, a savoir:
> 
> Lemma ext:(A,B:Set)(f,g:A->B)((a:A)(f a)=(g a))->f=g.

Cet axiome n'est pas prouvable en Coq.

Si tu penses a des fonctions comme des graphes (a l'ecole, en th. des
ensembles...) il est vrai. Si tu vois f et g comme des programmes, tu
n'as pas forcement envie de l'admettre. Heapsort et bubblesort ne sont
pas egaux, du point de vue de l'informaticien moyen. En coq, les
fonctions, et donc les algos, sont des objets primitifs, contrairement
aux mathematiques usuelles.


Pour certains travaux, cet axiome peut etre utile et tu peux
l'admettre sans crainte de casser la coherence du systeme logique
sous-jacent a Coq. 


La maniere completement orthodoxe est en general de definir la
relation d'equivalence consideree, puis de toujours raisonner modulo
cette relation. C'est un peu plus lourd et on pourrait esperer avoir
plus d'outils dedies dans le systeme dans le futur.

Donc il peut etre justifie d'admettre cet axiome.



Cordialement,



Benjamin Werner
----------------------------------------------------------------------------
Projet Coq
INRIA-Rocquencourt, BP 105, F-78 153 LE CHESNAY cedex, FRANCE
E-mail: 
Benjamin.Werner AT inria.fr
Phone:  +33 (1) 39 63 52 31
Mobile: +33 (6) 10 25 46 50
Fax:    +33 (1) 39 63 56 84
http://coq.inria.fr/~werner/
-----------------------------------------------------------------------------