The Coq mailing list

[Judicael Courant <jcourant AT lri.fr>]

In his message of Mon September 27, 1999, Jean-Christophe Filliatre writes: 
> 
> > 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.
> 
> This is not provable, since this not true. Indeed, equality means here
> convertibility  and you  may  have two  functions extensionally  equal
> without being convertible (as terms).
> 

Plus précisément, on peut choisir ou non d'accepter l'axiome
d'extensionnalité. Lorsqu'on a fait des maths "classiques", cet axiome
semble naturel : en fait c'est un théorème dès qu'on dit qu'une
fonction est simplement un graphe fonctionnel et que deux ensembles
sont égaux s'ils ont les mêmes éléments.

Dans un cadre informatique, où les fonctions sont des objets
primitifs, on peut décider qu'on ne veut pas de cette propriété : par
exemple un tri bulle n'est pas égal sous tous les plans à un tri
rapide : remplacer ce dernier par ce premier dans un programme peut
avoir des conséquences non négligeables. En Coq, cet axiome n'est donc
pas mis par défaut et il n'est pas démontrable.

Pour ce qui est de la cohérence logique de Coq avec un tel axiome, je
n'ai jamais entendu dire que la théorie devenait inconsistante
lorsqu'on rajoutait l'axiome d'extensionnalité mais je ne crois pas
avoir vu de résultat sur la consistance de Coq avec extentionnalité
non plus.

Cordialement,

Judicaël Courant.
-- 
Judicael.Courant AT lri.fr,
 http://www.lri.fr/~jcourant/
[Computing timetable constraints..................done: 0 solution(s)]