Merci pour ta réponse. En cherchant dans le manuel de référence Coq, j'ai fini par trouver la réponse à ma question:
C'est surtout la dernière ligne: because proofs can be eliminated only to build proofs évidemment qui indique clairement qu'on n'a pas de première projection pour les paires de Heyting. Dans ces conditions évidemment, proof-irrelevance ne pose pas de problème.Envoyé par Manuel de Référence Coq
J'ai regardé la FAQ Coq section 5.2 (Axiomes). Les axiomes énumérés ne créent effectivement aucune contradiction en présence des seuls principes intuitionnistes. Tous ces axiomes seront d'ailleurs imposés dans le système que j'ai en tête, sauf le tiers exclu et l'axiome du choix (functional axiom of choice dans la FAQ Coq), lequel entraine le tiers exclu par Diaconescu, ce qui fait que le tiers exclu ne sera pas primitif. Donc en fait, la seule option sera de savoir si on utilise l'axiome du choix ou non, c'est à dire si on fait des mathématiques classiques ou intuitionnistes. L'axiome du choix peut éventuellement s'éliminer lors de l'optimisation des preuves. On pourra donc faire des mathématiques intuitionnistes en utilisant l'axiome du choix. Il suffira de vérifier que le compilateur parvient à en élimliner toutes les instances.
Coq a donc abandonné la philosophie Martin-Löf (à quelle époque ?), puisque dans le système de Martin-Löf on a la première projection des paires de Heyting. C'est d'ailleurs cela qui fait que l'axiome du choix peut être prouvé (constructivement) en Martin-Löf, mais que bien sûr Diaconescu ne peut pas l'être. En effet, s'il l'était, le tiers exclu serait constructif.
Mon approche est évidemment différente des gens qui font de la théorie des types, puisque l'interprétation dans les topos sur laquelle je me base impose d'office proof-irrelevance. C'est une approche plus sémantique. Mais évidemment, elle ne donne aucune information sur la façon de calculer. Pour cela, il faut revenir à la théorie de la démonstration (normalisation forte).
Partager