Les subtilités de Coq, épisode 1 : élimination des sous-singletons

Je suis assez curieux des assistants de preuve. Jusqu'à il y a peu, je savais globalement me servir de Coq, mais ses fondements restaient assez obscurs pour moi : par exemple, pourquoi ces erreurs « non-strictly positive occurrence » au moment de définir un type inductif, « abstracting over the term "x" leads to a term which is ill-typed » en appliquant la tactic induction, ou encore « universe inconsistency » ? Quelles sont les règles de typage précises du calcul des constructions inductives ? Quelle sont les différences avec toutes ces théories des types dont j'entends parler : la théorie des types de Martin-Löf, la théorie des types homotopique, ou cubique, ou observationnelle ? Comment fonctionnent l'égalité et la tactique rewrite ? Pourquoi est-ce que les quotients sont si problématiques ? Plus récemment, en lisant certains billets de David Madore : quel rapport exact entre les topos élémentaires et les modèles de toutes ces théories des types ? Et cetera…

Je n'ai pas encore les réponses à toutes ces questions, mais je progresse, et je trouve que beaucoup des réponses sont très peu voire pas du tout expliquées de manière qui soit à la fois théorique et pédagogique : d'un côté, il y a les tutoriels de base des assistants de preuve qui donnent certaines intuitions sur des exemples vraiment simples sans expliquer le cas général, de l'autre côté il y a les articles de recherche en théorie des types, qui sont techniques à comprendre sans ces bases, et entre les deux… très peu de choses. Si je veux apprendre la topologie algébrique, je peux ouvrir un livre de 400 pages de topologie algébrique et commencer à lire la définition 1, le lemme 2 et la proposition 3, et j'ai largement de quoi m'occuper avant d'arriver au niveau où je devrai aller lire des articles de recherche pour comprendre les développements récents. Avec la théorie des types, malheureusement, il semble impossible de trouver un livre qui explique ne serait-ce que la différence entre le calcul des constructions et la théorie des types de Martin-Löf : on trouve des livres sur l'un et sur l'autre, mais rien qui daigne les comparer au lieu de laisser le lecteur jouer aux 7 différences entre leurs règles de déduction. Dans le même esprit, le paradoxe de Girard, qui est la raison fondamentale pour laquelle les univers de Coq sont organisés comme ils le sont, est expliqué clairement en à peu près un seul endroit, un article de Thierry Coquand de 1999 : on arrive, difficilement, à trouver comment les choses sont faites, mais trouver pourquoi elles ne pourraient pas être faites autrement ressemble à une sorte de grand jeu de piste.

Bref, je commence cette série de billets de blog pour essayer d'expliquer certaines choses que j'ai laborieusement fini par comprendre, en espérant que cela puisse être utile à d'autres. Je compte idéalement aller jusqu'aux définitions formelles du calcul des constructions, des pure type systems, des types inductifs, etc. Pour ce début, je reste très informel et « hands-on ».

Les exemples sont en Coq. La plupart ne sont pas propres à Coq et s'appliqueraient aussi en Lean ou d'autres implémentations du calcul des constructions inductives, mais Coq est celui que je connais le mieux, et il y a aussi des différences plus ou moins subtiles entre les deux qui seront vraiment importantes.

Merci beaucoup à tous ceux qui ont patiemment répondu à mes questions de théorie des types et m'ont suggéré des lectures. En espérant n'oublier personne : Gaëtan Gilbert, Arthur Adjedj, Thomas Lamiaux, Jean Caspar, Andreas Nuyts, Arnaud Spiwack, Naïm Favier, David Madore, Guillaume Melquiond, Kenji Maillard.

Ceci étant dit, attaquons le sujet de ce premier billet : l'élimination des sous-singletons. Pour l'introduire, je vais commencer par parler de l'égalité, qui est tout un sujet en soi (comme me disait mon tuteur de stage de L3, après 4000 ans de maths, on sait calculer la cohomologie étale des variétés

p

-adiques au-dessus du fibré en droites singulier des ∞-groupoïdes d'ultrafiltres monadiques, mais on ne sait toujours pas ce que veut dire

a = b

). Comme ce n'est pas le sujet principal ici, disons simplement que l'égalité en Coq est un type inductif avec un unique constructeur, eq_refl, de type @eq_refl : forall (A : Type) (x : A), x = x (le @ importe peu, il est là parce que les arguments sont marqués comme implicites), et que ce type inductif est défini dans la sorte Prop. Disons aussi que Prop est la sorte du « monde des preuves », qui est plus ou moins séparée du « monde calculatoire » Type, et notamment, une restriction importante empêche l'élimination forte de Prop, ce qui signifie concrètement qu'un pattern matching sur une valeur de type P où P : Prop doit obligatoirement renvoyer une valeur de type Q où Q : Prop. Par exemple, la définition suivante est rejetée car le pattern matching sur A \/ B : Prop renverrait une valeur de bool : Type.

Il se trouve que cette restriction évite un paradoxe, dont j'espère reparler dans un autre billet, mais on peut aussi se convaincre qu'elle est utile en se rappelant que Coq est capable de convertir une fonction de son langage en une fonction OCaml, ce qui s'appelle l'extraction (documentation), et dans ce processus d'extraction, les preuves de correction des algorithmes sont effacées pour ne garder que les algorithmes eux-mêmes. L'étanchéité entre Prop et Type s'assure que les algorithmes ne dépendent pas de la construction de leurs preuves.

Je vais partir de la question : pourquoi l'égalité est-elle ainsi définie comme un type inductif ?

En logique du premier ordre classique, le prédicat d'égalité est axiomatisé pour correspondre à l'égalité de Leibniz :

x

y

sont égaux si et seulement si ils ont exactement les mêmes propriétés. Au premier ordre, cette définition n'est pas pleinement satisfaisante pour la même raison que le schéma de récurrence de l'arithmétique de Peano n'exclut pas l'existence des modèles non-standard, à savoir que comme la logique manque de quantificateurs du second ordre, on ne peut pas définir l'égalité de manière interne (l'expression

∀ P, P(x) ⇒ P(y)

n'est pas du premier ordre), donc il faut postuler l'axiome de réflexivité (

∀ x, x = x

) et un schéma d'axiome de substitution

∀ x y, x = y ⇒ (P(x) ⇒ P(y))

pour chaque formule

P

du premier ordre. En revanche, dans un système aussi fort que Coq, largement plus fort que la logique du second ordre, on n'a besoin d'aucun axiome, on peut tout à fait définir directement un prédicat leibniz_eq par

et l'équivalent du schéma de substitution est exactement la définition. Il est donc naturel de penser que ceci pourrait être pris comme la définition du symbole «

=

» dans le calcul des constructions inductives. Pourtant cette définition ne fonctionne pas — ou du moins les choses sont nettement plus subtiles.

On pourrait penser que je pipote car, trivialement, l'égalité native de Coq est équivalente à l'égalité de Leibniz : sans même revenir à la définition de l'égalité native comme type inductif, en se rappelant intuitivement de ce qu'on peut faire avec elle, à savoir principalement appliquer la tactique rewrite, on voit facilement que si on a x = y et P : T -> Prop où T est le type de x et y, alors on obtient P x -> P y par rewrite à partir de la tautologie P x -> P x, et inversement, de forall P : T -> Prop, P x -> P y, on tire x = y en posant P := fun z => x = z et en appliquant l'hypothèse à la tautologie P x (qui se simplifie en x = x) pour obtenir P y (soit x = y). En somme :

Pourtant, je prétends que définir x = y comme leibniz_eq x y ne fonctionnerait pas, ou plutôt, que le faire sans définir à côté un type inductif d'égalité ne fonctionnerait pas.

Pour montrer que le problème n'est pas simplement théorique, je peux l'illustrer dans une situation très simple mais néanmoins réaliste. On souhaite prouver l'associativité de la concaténation de listes, sur un type de listes polymorphe qui contient leur longueur, c'est-à-dire un type inductif paramétré par un type pour les éléments et indexé par un entier

n

qui est la longueur des listes habitantes du type⁰. On définit la fonction concat de la manière évidente (et en mode preuve pour éviter le pattern matching dépendant que je dois expliquer dans un autre billet) :

Maintenant, on peut tenter de prouver l'associativité — seulement l'énoncé même du théorème ne type pas :

En effet, on a écrit une égalité entre termes de types list_n T (n1 + (n2 + n3)) et list_n T ((n1 + n2) + n3), or ces types sont propositionnellement égaux, au sens où on peut prouver l'égalité list_n T (n1 + (n2 + n3)) = list_n T ((n1 + n2) + n3), mais il ne sont pas définitionnellement égaux, c'est-à-dire convertibles (au sens de la β-équivalence du λ-calcul, qui en fait est plutôt ici la βδζιη-équivalence parce qu'il y a des règles en plus), et donc on ne peut pas écrire d'égalité entre les deux car l'égalité demande deux termes du même type.

En somme, il faut commencer par écrire une fonction auxiliaire qui transtype lst2. On le fait facilement en mode preuve grâce à rewrite, et on peut alors énoncer le théorème :

Je ne vais pas faire la preuve de concat_assoc ; intéressons-nous plutôt à la manière dont l'égalité est utilisée pour ce transtypage. Un Print convert. nous montre le terme de preuve :

On voit apparaître le terme eq_rect_r, qui ressemble énormément à leibniz_eq :

et on peut tenter d'appliquer la même structure avec leibniz_eq (je mets l'égalité de Leibniz entre (n1 + n2) + n3 et n1 + (n2 + n3) en argument pour simplifier, on pourrait bien sûr la reprouver) :

Voilà donc le cœur du problème : l'égalité de Leibniz sous la forme forall P : T -> Prop, P x <-> P y permet uniquement de convertir P x en P y quand P x vit dans Prop. On peut d'ailleurs insérer Unset Universe Checking. avant la définition pour constater qu'en oubliant temporairement la différence entre Prop et Type, elle type bien. Bref, elle ne permet pas de faire des transtypages en dehors de Prop. (En l'occurrence, l'énoncé de concat_assoc est dans Prop, donc on pourrait s'en sortir en déplaçant toute la conclusion du théorème à l'intérieur de l'invocation de E, mais ça ne permet pas de définir la fonction convert séparément de concat_assoc, et dans un contexte de vérification de programme, où on se sert d'un transtypage pour montrer un invariant qui justifie que l'étape suivante est bien définie, ça ne marcherait pas du tout.)

Dans ce cas, Coq rejette la définition parce que ce code essaie de mettre l'égalité dans Prop alors qu'elle quantifie sur A -> Type qui est dans Type. Or on ne veut certainement pas que x = y vive dans Type, car x = y est l'archétype de ce qu'on pense comme une proposition.

On voit donc que derrière l'égalité définie par un type inductif se cache une sorte de magie. D'un côté, le type inductif vit dans la sorte Prop :

Avec simplement des codages à la leibniz_eq, cette paire de fonctions eq_refl, eq_rect_r ne serait pas définissable. Où est le truc ?

Honnêtement, je trouve la raison pour laquelle eq_rect_r existe assez décevante. Je voyais le calcul des constructions inductives comme un système de typage très élégant, symétrique, …, et ici on a presque l'impression d'un « bricolage ».

La réponse est que eq_rect_r est l'éliminateur du type inductif d'égalité (ou presque, c'est plutôt eq_rect, qui met le x = y dans l'autre sens), et qu'il y a un cas particulier qui permet d'éliminer un type inductif dans Prop vers Type, lorsqu'il vérifie une condition syntaxique dite de sous-singleton, à savoir : soit le type n'a aucun constructeur, soit il a un unique constructeur dont tous les arguments sont aussi dans la sorte Prop.

Cette condition, qui est purement syntaxique, est censée assurer que l'élimination ne va pas révéler d'informations au monde calculatoire Type sur la valeur qui était dans le monde logique Prop. Dans le cas sans aucun constructeur, il n'y a de toute façon aucun habitant du type (l'hypothèse est absurde). Avec un unique constructeur, on ne révèle d'abord pas l'information du constructeur choisi pour former la preuve — ce qui par exemple pour A \/ B reviendrait à savoir quelle possibilité a été prouvée, rendant ce type moralement équivalent à {A} + {B}. Comme les arguments sont dans Prop, récursivement, on ne peut rien en faire sauf les éliminer aussi comme sous-singletons, ce qui à nouveau n'apporte rien — alors que par exemple éliminer exists, de constructeur ex_intro : forall {A : Type} (P : A -> Prop) (x : A), P x -> exists y, P y, donnerait accès au témoin que renferme la preuve, ce qui permettrait de prouver l'axiome du choix.

Le cas sans constructeur correspond à l'élimination de False, qui est justement défini par la déclaration Inductive False : Prop := . (dont la syntaxe peut faire lever un sourcil la première fois). Là aussi, on aurait du mal à s'en passer. Cette élimination forte de False permet, dans un programme, de ne pas avoir à trouver une valeur à renvoyer dans un cas qui ne peut jamais se produire à cause d'un invariant. Un exemple réaliste est le suivant, où je l'utilise plusieurs fois pour récupérer le

n

-ième élément d'une liste sous la condition que

n

est dans les bornes de la liste. L'élimination de False permet de se débarrasser des branches absurdes où on se rend compte que

n

est en dehors de ces bornes. Comme T est un type général (qui est possiblement inhabité, et dont on n'a de toute façon pas d'habitant à disposition), il n'y a aucun moyen de faire autrement.

Il me semble que ce concept d'« élimination des sous-singletons » est assez mal nommé, car le lien avec le concept de sous-singleton en maths constructives est beaucoup plus ténu que le nom veut le laisser croire. Certes, ce terme de « sous-singleton » est déjà contentieux en maths constructives (un peu comme l'éternel problème des compacts qui sont supposés séparés ou non…) car «

X

est un sous-singleton » signifie, selon les auteurs, soit que

∀ x x' ∈ X, x = x'

, soit parfois, dans le contexte où

X

est un sous-ensemble d'un autre ensemble

Y

, que

∃ y ∈ Y, ∀ x ∈ X, x = y

; mais en l'occurrence, il n'y a pas de sur-ensemble ambiant, c'est donc clairement la première notion que le terme évoque. Or il n'y a pas d'inclusion, ni dans un sens ni dans l'autre, entre les inductifs T tels que prouvablement forall x x' : T, x = x' et les inductifs auxquels s'applique l'élimination des sous-singletons.

Avant tout, l'axiome d'indiscernabilité des preuves (ceci est une tentative de traduction de proof irrelevance) est précisément l'affirmation qu'absolument toutes les propositions sont des sous-singletons. On peut parfaitement travailler sous cet axiome, c'est même courant, et cela n'entraîne certainement pas qu'il soit permis d'éliminer exists x, P x pour obtenir l'axiome du choix !

Même sans indiscernabilité des preuves, il y a des sous-singletons qu'on ne veut pas rendre éliminables vers Type. Un exemple est le type d'inégalité large n <= m, où n et m sont deux entiers. Il est défini par deux constructeurs :

On peut prouver que pour tous n, m, le type n <= m est un sous-singleton — c'est le lemme Peano_dec.le_unique de la bibliothèque standard de Coq. La preuve n'est absolument pas aussi triviale qu'il paraît (j'espère en reparler dans un futur billet sur les types inductifs et le pattern matching dépendant), mais c'est néanmoins vrai, et l'intuition, bien sûr, est que pour n et m fixés, un seul des deux cas peut s'appliquer, à savoir le_n si

n = m

et le_S si

n < m

. Or, pour la même raison, l'élimination forte sur n <= m permettrait, à partir d'une preuve de n <= m, de retrouver dans le monde calculatoire si

n = m

. Clairement, cela empêcherait l'effacement du calcul de la preuve à l'extraction, puisqu'il faudrait construire effectivement l'objet n <= m pour regarder de quel constructeur il est fait (ou alors insérer un test en

O(n)

de l'égalité

n = m

, ce qui n'est pas vraiment l'idée qu'on se fait d'un simple pattern matching !).

Dans l'autre direction, si l'on ne suppose pas l'indiscernabilité des preuves, alors P /\ Q n'est pas prouvablement un sous-singleton en général, car P et Q pourraient chacune avoir plusieurs preuves, et pourtant l'élimination « des sous-singletons » est bel et bien autorisée sur P /\ Q, l'idée étant qu'elle va juste révéler la preuve de P et la preuve de Q, sans descendre plus profondément, et qu'on ne peut donc pas extraire d'information calculatoire intéressante puisqu'on ne pourra pas éliminer ces deux preuves elles-mêmes (sauf par élimination des sous-singletons, récursivement).

Je peux aussi mentionner le cas un peu curieux du type d'existence unique exists! x, P x. « Moralement », si ce type est habité, on a une forme faible d'unicité de la preuve car le témoin x est unique, puisqu'il est accompagné par définition d'une preuve de son unicité. Pourtant, l'élimination forte sur tous ces types permettrait de prouver l'axiome du choix unique (ou axiome du non-choix). La réalité est un peu plus compliquée que cette morale car pour que exists! x, P x soit effectivement un sous-singleton quand il est habité, il faut aussi l'égalité entre toutes les preuves que x vérifie P et est unique. Néanmoins, sous l'axiome d'extensionnalité fonctionnelle (dépendante), qui est (me semble-t-il) moralement orthogonal à l'indiscernabilité des preuves, on peut le prouver en faisant les hypothèses supplémentaires que les preuves d'égalité sur le type de x sont uniques, et que P x est lui-même un sous-singleton. Il se trouve que l'unicité des preuves d'égalité est vérifiée (sans hypothèse supplémentaire) dans le cas particulier du type nat, ce qui permet de donner un exemple non-trivial :

On voit que, sous le seul axiome d'extensionnalité fonctionnelle, j'ai prouvé que pour tout n, le type exists! k, n = 2*k est un sous-singleton. Pour n pair, il est habité. Si on pouvait l'éliminer, on aurait une instance particulière de l'axiome du choix unique qui donnerait calculatoirement accès à la moitié d'un entier à condition qu'il soit pair (la preuve par récurrence correspond à l'algorithme évident qui garde un successeur sur deux), et à nouveau, ceci est totalement incompatible avec l'effacement des preuves à l'extraction.

Finalement, plutôt que « élimination des sous-singletons », j'aurais tendance à parler d'« élimination non-informative », ou bien d'« élimination forte effaçable » pour souligner que bien qu'il s'agisse d'une élimination forte, elle reste compatible avec l'effacement de Prop à l'extraction. Dommage qu'on ne puisse pas refaire la terminologie en vigueur…

Je conclus là sur l'élimination des sous-singletons. Si je trouve le temps, je reparlerai de l'unicité de n <= m dans un billet plus général sur les types inductifs, et de l'élimination forte dans un autre billet sur le paradoxe de Girard.

Mise à jour (4 novembre 2024) : Quelques corrections et clarifications suite à cette discussion (j'ai aussi fait des corrections et modifications mineures que je ne crois pas utile de marquer).

Commentaires

# Commentaire de Gro-Tsen (4 novembre 2024 à 16:11)

La condition exists x : T, forall y : T, x = y définit un singleton, pas un sous-singleton : le type est habité et tous ses éléments sont égaux, c'est exactement un singleton. Là où il y a un doute sur la notion de sous-singleton, c'est entre la notion absolue de type T dont tous les éléments sont égaux entre eux (∀x:T.∀y:T.x=y) et la notion relative de partie S d'un type X dont tous les éléments sont égaux à un certain élément du type (∃x:X.∀y∈S.x=y) ; mais cette dernière notion n'a pas de sens pour un type dans l'absolu (et comme je ne sais pas comment traduire correctement la notion de partie d'un ensemble en Coq, je ne sais pas la dire en Coq du tout).

Pour ce que ça vaut, on peut appeler “flasque” (cf. ici sur MathOverflow et la réponse qu'on m'a faite) un X dont toute partie S⊆X telle que ∀x∈S.∀y∈S.x=y vérifie ∃x:X.∀y∈S.x=y. Pour ce que ça vaut aussi, en IZF, l'univers des ensembles est flasque en ce sens, c'est-à-dire que si on a un ensemble S dont tous les éléments sont égaux (∀x∈S.∀y∈S.x=y), alors il existe un ensemble x tel que ∀y∈S.x=y, bref, S⊆{x} ; pour la preuve, il suffit d'utiliser l'axiome de l'union pour former la réunion x de tous les éléments de S, et si y∈S alors tout élément de S est égal à y donc la réunion vaut y, bref, x=y, ce qui montre bien que S⊆{x}.

# Commentaire de Gro-Tsen (4 novembre 2024 à 16:58)

Bon, et sinon j'avoue ne pas vraiment comprendre ce que c'est, en fait, que l'« extraction ». Dans mon esprit, un des trucs du constructivisme, c'est que si on prouve ∀x:X.∃y:Y.P(x,y) alors on doit pouvoir extraire de la preuve une fonction X→Y (et c'est un théorème de certaines théories de maths constructives, par exemple beaucoup de variantes de l'arithmétique de Heyting avec X et Y étant le type des naturels). Mais là tu dis quelque chose de différent : « convertir une fonction de son langage [Coq] en une fonction OCaml » — mais si Coq est juste un langage de programmation, ça ça correspond juste à une conversion d'un langage vers un autre, non ? Il n'y a pas de magie constructive particulière, on oublie juste les preuves dont OCaml n'a rien à faire. Bon, il faudrait deux mots pour désigner ces deux choses qui sont visiblement différentes mais dont le rapport exact m'échappe : appelons-les extraction₁ (celle qui prend une preuve constructive et extrait un programme) et extraction₂ (celle qui prend un programme en Coq et extrait un programme en autre chose) for lack of something better.

L'autre chose, donc, c'est que je ne vois pas en quoi l'axiome du choix unique pose problème par rapport à ça. Dans le cas de l'extraction₁ il y a éventuellement un problème qui est que si on a prouvé ∀x:X.∃y:Y.P(x,y) il faut regarder à l'intérieur de la preuve quel y est construit pour un x donné afin d'extraire une fonction X→Y, mais justement si on a ∀x:X.∃!y:Y.P(x,y) ce problème disparaît et la fonction ne dépend plus de la preuve (au moins en extension). Dans le cas de l'extraction₂ je vois encore moins le problème puisqu'on a, justement, un algorithme qui construit y et on cherche juste à oublier la preuve de l'unicité du y calculé par l'algorithme. Donc je ne comprends pas ton argument comme quoi ce serait « totalement incompatible avec l'effacement des preuves à l'extraction » (enfin, je vois bien pourquoi ce n'est pas à partir de la simple certitude que ∀x:X.∃!y:Y.P(x,y) est prouvable qu'on va extraire une fonction X→Y, mais justement, l'extraction₁ est censée tirer un algorithme de la preuve et l'extraction₂ est simplement censée tirer un algorithme… d'un autre algorithme écrit en Coq ; est-ce qu'il y a une extraction₃ encore différente de ces deux choses ? tout ça est terriblement confus pour moi). Disons que j'ai plutôt l'impression que ce qui pose problème est l'indiscernabilité des preuves qui empêche d'extraire l'algorithme de la preuve, pas l'axiome du choix unique.

(Il y a une discussion ici sur MathOverflow sur ce que ça signifie de faire des maths sans l'axiome du choix unique, mais elle ne m'a pas vraiment Éclairé. Je note quand même la comparaison avec la géodiff, où ce n'est pas parce que pour tout x dans une variété X il existe un unique y dans Y telle que (x,y) appartienne à une sous-variété P qu'on peut pour autant trouver une fonction lisse x↦y. Mais je ne sais pas si ça représente bien le problème ici.)

Fondamentalement, le souci est que je ne sais pas ce que Coq appelle X→Y. Qu'est-ce que cette flèche signifie, au juste ? En maths, une fonction est quelque chose d'extensionnel, donc elle est déterminée par son graphe et elle n'est rien de plus que son graphe. En Coq, on essaie de capturer… quoi exactement ? Je pourrais être tenté d'imaginer que nat->nat ce sont les algorithmes qui prennent un entier naturel et renvoient un entier naturel (ça explique certainement l'absence d'extensionalité fonctionnelle), mais ce n'est pas ça non plus, parce que dans ce cas le principe de Church-Turing devrait être automatique, ce qui n'est pas le cas. Formellement, X→Y est défini par des règles de typage, donc c'est juste « le type dans lequel vivent les termes qu'on arrive à fabriquer avec ces règles de typage », mais ces règles et ce type essaient de faire quoi, si ce n'est ni extensionnel ni une notion d'algorithme ?

En tout cas, je ne peux pas m'empêcher de penser que si l'axiome du choix unique n'est pas prouvable, c'est que le système de types est fondamentalement cassé (la notion de fonction est incompatible avec la notion de preuve, donc forcément le mélange a des propriétés complètement merdiques). Manifestement les gens qui font de la théorie homotopique des types ont l'air de penser pareil parce que le principe de choix unique est prouvable dans leur machin (que je ne prétends pas comprendre, enfin, encore moins que Coq, quoi) : corollaire 3.9.2 du livre Homotopy Type Theory. Mais est-ce que ça veut dire qu'ils ont renoncé à quelque chose que Coq permet ? Je n'en ai aucune idée.

# Commentaire de Jean Abou Samra (4 novembre 2024 à 18:09)

La condition exists x : T, forall y : T, x = y définit un singleton, pas un sous-singleton

Ouhlà, ce que je n'ai écrit n'a aucun sens, je ne sais pas comment j'ai pu m'embrouiller comme ça ! Je corrige. (Et je réponds au reste plus tard.)

# Commentaire de Jean Abou Samra (4 novembre 2024 à 20:44)

mais cette dernière notion n'a pas de sens pour un type dans l'absolu (et comme je ne sais pas comment traduire correctement la notion de partie d'un ensemble en Coq, je ne sais pas la dire en Coq du tout).

Pour le coup, je ne crois pas que l'analogie avec les topos pose de problème particulier, si ? De même que dans un topos, une partie de X s'assimile à une fonction X → Ω vers l'objet des valeurs de vérité Ω, les parties d'un type X en Coq s'assimilent aux habitants de X -> Prop. C'est ce qu'on voit un peu partout.

Là où il y a un souci dans l'analogie, c'est avec les parties décidables, qui dans un topos sont les fonctions Χ → 2, sachant qu'en Coq, pour convertir P : X -> Prop en X -> bool, il faut non seulement forall x, P x \/ ~(P x) mais en fait forall x, {P x} + {~(P x)}, distinction qui n'existe pas dans les topos.

# Commentaire de Jean Abou Samra (4 novembre 2024 à 22:26)

Sur l'extraction. Tu me pardonneras de raconter des choses dont une partie sont sans doute évidentes pour toi, mais en fait j'avoue que j'ai un peu du mal à comprendre ta confusion, donc je ne sais pas quels détails je dois donner.

Ce que tu appelles extraction₁ est en un certain sens la fonction identité étant donné que du point de vue de Coq, la preuve de ∀ x, ∃ y, P(x, y) est par définition un terme que tu peux appliquer, à condition qu'il soit clos et notamment qu'il ne contienne pas d'axiome. En pratique ce n'est pas tout à fait vrai parce que la plupart des théorèmes sont finis par Qed., ce qui rend le terme de preuve « opaque » (Coq va refuser de le réduire en sa définition), ça sert à ce que l'interface du théorème soit juste son type, sinon ses utilisateurs pourraient potentiellement prouver des choses qui dépendent de son terme de preuve, et ensuite, tu changerais la preuve sans changer l'énoncé et ça casserait des choses ailleurs. Mais ce n'est qu'un détail pratique, et du moment que tu termines les théorèmes par Defined., tu peux juste demander à Coq de réduire l'application du terme du théorème à un x donné. Donc pour qu'on soit bien d'accord sur le sens des mots, si j'ai bien compris ce que tu appelles extraction₁, c'est ça :

Example div2 : forall n : nat, exists k : nat, n = k*2 \/ n = S (k*2).
Proof.
  induction n as [|n IH].
  - exists 0. left. reflexivity.
  - destruct IH as [k [eq_even | eq_odd]].
    + exists k. right. rewrite eq_even. reflexivity.
    + exists (S k). left. rewrite eq_odd. reflexivity.
Defined.

Compute (div2 100).
(* = ex_intro (...) 50 (...) : ...

Si tu veux rendre ça plus lisible, tu peux faire

Definition keep_only_witness
  {A : Type} {P : A -> Prop} (proof : exists x, P x)
  : inhabited A
  := let (x, _) := proof in inhabits x.

Compute (keep_only_witness (div2 100)).
(* = inhabits 50 : inhabited nat *)

(sachant que le type inhabited sert juste à rester dans Prop parce qu'on ne peut pas s'en échapper justement à cause de la restriction sur l'élimination forte).

Maintenant, l'extraction₂, c'est ce que j'appelais juste extraction dans le billet, mot qui dans le contexte de Coq désigne le mécanisme qui est documenté ici : https://coq.inria.fr/doc/V8.20.0/refman/addendum/extraction.html (j'ai rajouté le lien dans le billet). C'est bien une conversion du langage des termes de Coq (nommé « Gallina ») en langage OCaml, et ce n'est pas si simple que ça, à cause des types dépendants que n'a pas OCaml et qui forcent le convertisseur à mettre des transtypages Obj.magic un peu partout (qu'OCaml ne peut pas vérifier, ce qui n'est pas grave parce qu'ils ont été vérifiés par Coq), mais néanmoins le simple fait de convertir en OCaml ne pose pas de difficulté théorique essentielle. Par contre, comme tu l'as bien compris, la particularité de cette conversion est d'effacer les preuves, ce qui veut concrètement dire que toutes les parties du terme à extraire qui vivent dans la sorte Prop vont être virées à la conversion, et il faut que Gallina soit compatible avec ça.

En soi, on pourrait garder les preuves, ça ne poserait pas de problème particulier, mais le rôle de Prop est en partie de servir de marqueur de ce qu'on veut garder à l'extraction ou pas. Si tu écris une bibliothèque, ça peut être une bonne idée de faire un minimum attention à l'efficacité algorithmique de ce qui vit en dehors de Prop, alors que dans Prop on s'en fiche complètement. Par exemple, le code précédent peut aussi se réécrire

Require Import Lia.

Example div2 : forall n : nat, exists k : nat, n = k*2 \/ n = S (k*2).
Proof.
  induction n as [|n IH].
  - exists 0. lia.
  - destruct IH as [k [eq_even | eq_odd]].
    + exists k. lia. 
    + exists (S k). lia. 
Defined.

sauf que là, si je fais Compute (div2 100)., je dois l'arrêter avant que mon ordinateur se mette à chauffer trop. Si tu regardes le terme de preuve avec Print div2., tu verras qu'il est monstrueux (c'est d'ailleurs un peu surprenant que ce soit à ce point), mais je ne peux pas reprocher grand-chose aux auteurs de lia., parce que leur tactique produit du Prop, donc je ne dois pas m'attendre à ce que ce le terme de preuve soit particulièrement efficace en tant que programme, juste à ce qu'il soit typable en un temps raisonnable.

D'autre part, tu pourrais très bien faire des preuves dans Type en y redéfinissant les connecteurs usuels ; ce serait plutôt du raisonnement à la MLTT à cause de la prédicativité de la hiérarchie de Type, mais je ne crois pas que ce soit fondamental ici.

Du coup, je ne comprends pas trop la manière dont tu sembles faire une distinction entre « extraire les preuves » qui serait difficile (« magie constructive ») et extraire les programmes qui serait facile (« juste une conversion d'un langage vers un autre »), parce qu'on a deux mondes « preuves » et « calculs » qui sont plus ou moins isomorphes, modulo ces histoires d'imprédicativité ; dans les deux cas les preuves/algorithmes sont représentés par des termes, et ils sont surtout distingués par leur usage pratique. Et s'il y a un côté où c'est plus difficile que l'autre de faire de l'extraction, c'est plutôt le côté calculs, parce qu'on veut pouvoir l'extraire d'une manière qui le sépare du côté preuves.

Ensuite, sur l'axiome du choix unique.

Déjà, je dois mal interpréter ce que tu écris là-dessus parce que je ne saisis pas ton argument sur le fait que l'axiome du choix unique devrait être prouvable. Je ne comprends pas en quoi ça diffère de l'argument dont tu sais bien évidemment qu'il n'a pas de sens : « je raisonne en logique intuitionniste ; si j'ai ∀ x, ∃ y, P(x, y), alors comme “tout est constructif”, j'ai un moyen effectif de construire y à partir de x, c'est bien une fonction f telle que ∀ x, P(x, f(x)), donc l'axiome du choix est vrai (et avec lui le tiers exclu par Diaconescu) ». Je ne vois pas en quoi l'unicité y change quoi que ce soit (d'accord, ça dit que la fonction est unique dans une vision extensionnelle, mais en quoi ça aide à l'obtenir ?).

Il faut quand même distinguer d'un côté l'extraction d'une preuve complète terminée, qui est un terme clos, et de l'autre l'axiome du choix, unique ou non, qui s'applique n'importe où dans n'importe quel contexte de preuve, possiblement incohérent, et où en tous cas les fonctions X → Y sont pensées comme quelconques et pas spécialement constructibles en quelque sens que ce soit (pour la même raison qu'on ne peut pas prouver et qu'on ne suppose usuellement pas la thèse de Church-Turing étendue en Coq).

Tu as néanmoins parfaitement raison de relever ma phrase « on aurait une instance particulière de l'axiome du choix unique […] ceci est totalement incompatible avec l'effacement des preuves à l'extraction » parce qu'effectivement, si tu postules l'axiome du choix unique sous la forme

Axiom unique_choice :
  forall {X Y : Type} (P : X -> Y -> Prop),
    (forall x, exists! y, P x y) ->
    exists (f : X -> Y), forall x, P x (f x).

alors comme il renvoie du Prop, c'est compatible à l'extraction. Le truc, c'est que j'avais plutôt en tête cette forme :

Axiom unique_choice :
  forall {X Y : Type} (P : X -> Y -> Prop),
    (forall x, exists! y, P x y) ->
    {f : X -> Y | forall x, P x (f x)}.

qui elle ne l'est pas, parce que {x | P x} vit dans Type et on peut extraire son x. Malheureusement, on n'a pas de mot français pour exprimer la distinction ∃/Σ. L'élimination forte de exists! prouverait aussi cette deuxième forme.

Tu demandes ce que « veut dire » X → Y en Coq. Je pourrais répondre que c'est comme les termes du λ-calcul, on les manipule syntaxiquement, et pour savoir ce qu'ils « veulent dire », il faut regarder les modèles (et l'invention de modèles du λ-calcul date de bien plus tard que son invention syntaxique), ou bien comme la négation en logique intuitionniste (même remarque), et qu'il faut juste s'habituer à raisonner dans un monde différent où les intentions comptent (est-ce une morale sur la préméditation en droit ?). Mais ce serait une réponse malhonnête parce qu'en vrai, je suis trouve aussi énervante cette absence d'extensionnalité, et d'ailleurs je crois avoir vu passer sur Mastodon un théoricien des types qui disait quelque chose comme « funext and propext are useful enough that people keep trying to invent type theories which satisfy them ».

Par contre, je peux donner un élément d'intuition sur au moins une bonne raison pour laquelle ça peut être embêtant d'ajouter l'extensionnalité fonctionnelle (en espérant ne pas dire de bêtises parce que je ne comprends pas tout ça super bien non plus), c'est que ça casse la propriété de canonicité, c'est-à-dire le fait que la forme normale de tout terme clos de type nat est toujours de la forme S (S (S (... 0 ... ))). Cette extensionnalité fonctionnelle n'est pas un axiome intrinsèquement non-constructif, au sens où il n'empêche pas d'extraire un algorithme, mais le hic, c'est que l'algorithme ne correspond plus exactement au λ-terme de preuve. Exemple concret adapté de https://leanprover.github.io/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality :

Axiom funext : forall {X : Type} {Y : X -> Type} (f g : forall x, Y x),
    (forall x, f x = g x) -> f = g.

(* silly_inductive unused U wraps a value of type U. It has an unused parameter. *)
Inductive silly_inductive {U : Type} (unused : U) (T : Type) :=
| make_silly : T -> silly_inductive unused T.

Definition id1 (x : nat) := x.
Definition id2 (x : nat) := x.

Fact eq_id12 : id1 = id2.
Proof.
  apply funext. reflexivity.
Defined.

Definition silly_zero1 : silly_inductive id1 nat := make_silly id1 nat 0.
Definition silly_zero2 : silly_inductive id2 nat.
Proof.
  rewrite <- eq_id12. exact silly_zero1.
Defined.

Definition unwrapped_zero := match silly_zero2 with make_silly _ _ x => x end.

Compute unwrapped_zero.

La dernière ligne donne

     = match
         match
           funext (fun x : nat => x) (fun x : nat => x) (fun x : nat => eq_refl) in (_ = H)
           return (silly_inductive H nat)
         with
         | eq_refl => make_silly (fun x : nat => x) nat 0
         end
       with
       | make_silly _ _ x => x
       end
     : nat

Ce terme ne se simplifie pas parce que ce que renvoie funext est opaque, il n'y a pas de moyen de le prouver égal à eq_refl sans l'axiome d'unicité des preuves d'égalité. En réalité, même en le prenant comme axiome, ça ne marcherait pas, il faudrait que l'égalité entre funext ... et eq_refl soit non seulement propositionnellement prouvable mais qu'en fait funext ... se réduise en eq_refl, et en particulier qu'il y ait égalité définitionnelle entre les deux. Et c'est très facile, en mettant un peu trop d'égalité définitionnelle, de rendre la vérification du typage indécidable ou de casser d'autres propriétés fondamentales du système. C'est notamment ce que fait Lean, ils ont mis la proof irrelevance définitionnelle dans l'équivalent du Prop de Coq (je dois dire que c'est assez YOLO) et du coup ils cassent tout à la fois

La décidabilité du type-checking,
L'autoréduction (subject reduction) en pratique, parce que le type-checking est une approximation décidable d'un problème indécidable,
Et aussi la transitivité de l'égalité définitionnelle, pour la même raison,

le dernier point signifiant qu'il est possible que l'équivalent de assert (x = y) by reflexivity. fonctionne et aussi assert (y = z) by reflexivity. mais pas assert (x = z) by reflexivity.

En Coq, il y a un univers parallèle à Prop qui s'appelle SProp et qui a la proof irrelevance définitionnelle, mais d'une manière qui ne casse pas tout ça, et pour l'instant je ne me suis pas plongé dans les différences. L'article est là https://inria.hal.science/hal-01859964v1/file/main_popl.pdf et la documentation ici https://coq.inria.fr/doc/V8.20.0/refman/addendum/sprop.html.

Mais ce qui est amusant, c'est que si tu fais

Require Import Extraction.
Recursive Extraction unwrapped_zero.

tu te retrouves avec

type nat =
| O
| S of nat

type ('u, 't) silly_inductive = 't
  (* singleton inductive, whose constructor was make_silly *)

(** val silly_zero1 : (nat -> nat, nat) silly_inductive **)

let silly_zero1 =
  O

(** val silly_zero2 : (nat -> nat, nat) silly_inductive **)

let silly_zero2 =
  silly_zero1

(** val unwrapped_zero : nat **)

let unwrapped_zero =
  silly_zero2

où, comme attendu, l'effacement de tout ce qui est dans Prop, en particulier du résultat de funext, fait que unwrapped_zero peut bien être calculé en 0 par OCaml.

# Commentaire de DmxLarchey (7 novembre 2024 à 12:19)

@Gro-Tsen,

Il me semble que si on combine Unique Choice (UC) avec eXcluded Middle (XM), on peut montrer l'existence de fonctions non-calculables.

Par exemple, avec XM uniquement, on peut prouver le lemme de König sur les arbres binaires et construire une branch infinie (d'un arbre binaire non borné) sur la forme d'une relation fonctionnelle totale G : nat -> bool -> Prop, càd qui vérifie forall n, exists! a, G n a.

UC permet alors de réifier cette relation G en 'f : nat -> boolavecG n (f n)`.

Or Kleene a construit un arbre binaire infini décidable dont aucune branche infinie n'est calculable. Ce qui implique dans ce cas que f au dessus ne peut pas être extraite.

Bien-sûr on parle ici d'une combinaison XM + UC.

D. Larchey-Wendling

# Commentaire de Jean Abou Samra (7 novembre 2024 à 16:59)

@Dominique : Merci pour votre commentaire, c'est une jolie construction.

Il me semble qu'on peut en donner une autre qui est sans doute plus simple (pas besoin de ce théorème de Kleene), mais je me suis peut-être trompé quelque part. Prenons une machine de Turing et considérons l'ensemble des n tels que la machine a terminé au bout de n étapes. Sous le tiers exclu, cet ensemble est vide ou habité. Dans le deuxième cas, il a un minimum : on pourrait avoir l'impression à première vue qu'il faudrait l'axiome du choix dépendant pour le prouver, mais ce n'est pas le cas (le tiers exclu suffit), car s'il n'a pas de minimum, on peut montrer par récurrence forte qu'aucun élément n'est dans l'ensemble (sinon c'est un minimum par hypothèse de récurrence), contredisant l'hypothèse qu'il est habité. Donc, l'unicité d'un minimum étant claire, on devrait pouvoir prouver :

forall M : TuringMachine,
  exists! result : option nat,
    match result with
      | None => ~exists n, terminates_in_n_steps M n
      | Some n => terminates_in_n_steps M n /\ forall m, m < n -> ~terminates_in_n_steps M m
    end

et on peut alors appliquer le choix unique pour obtenir une fonction non-calculable. 30|En fait je ne sais pas pourquoi je suis allé chercher cette histoire de minimum alors que c'est encore plus trivial que ça : forall M : TuringMachine, exists! terminates : bool, (exists n, terminates_in_n_steps M n) <-> (terminates = true).

# Commentaire de Jean Abou Samra (8 novembre 2024 à 12:30)

En fait je ne sais pas pourquoi je suis allé chercher cette histoire de minimum alors que c'est encore plus trivial que ça : forall M : TuringMachine, exists! terminates : bool, (exists n, terminates_in_n_steps M n) <-> (terminates = true).

# Commentaire de Gro-Tsen (10 novembre 2024 à 21:11)

Je ne vais pas faire une réponse longue pour expliquer pourquoi je ne comprends toujours pas le problème avec le choix unique pour l'extraction dans Coq, parce que ça va surtout révéler que je ne connais vraiment pas grand-chose à Coq, et ce n'est pas très intéressant à raconter vu que j'ai juste très peu de temps pour m'y intéresser (à vrai dire j'ai beaucoup de mal à lire les exemples, vu que je connais mal même la syntaxe, et aussi que les successions de tactiques sont hyper difficiles à suivre et que je sais à peine lancer le programme pour les essayer). Je suis aussi perdu dans un labyrinthe d'hypothèses qu'on peut ou peut ne pas mettre (entre la proof irrelevance, l'extensionalité propositionnelle, l'extensionalité fonctionnelle, l'axiome du choix ou juste l'axiome du choix unique…) et dont je n'ai aucune idée de comment elles interagissent au sein de Coq.

Mais à un niveau plus large, et je vais plutôt ranter là-dessus, je ne sais juste pas ce que le Prop (ou le SProp, puisqu'il y a ça, maintenant) de Coq est censé représenter ou modéliser, intuitivement, ni, en fait, le signe ‘->’. (Par exemple, j'ai une certaine intuition sur le principe de Markov en maths constructives. Mais j'ai exactement zéro intuition sur la différence entre sa formulation comme forall p:nat->Prop, (forall n:nat, (p n)\/~(p n)) -> (~ forall n:nat, (p n)) -> (exists n:nat, ~(p n)) et comme forall p:nat->bool, (~ forall n:nat, (p n)=true) -> (exists n:nat, (p n)=false) an Coq. Ni sur comment diable on peut prouver que ces choses ne sont pas démontrablement équivalentes. C'est quoi la différence intuitive entre un booléen et une proposition qui est soit vraie soit fausse ?)

Un topos, je comprends ce que c'est pour plusieurs raisons. Déjà, la définition n'est pas atrocement compliquée (c'est une catégorie admettant les limites finies, des exponentielles et un objet classifiant les sous-objets c'est-à-dire les classes d'équivalences de monomorphismes) ; mais surtout, on peut donner des exemples assez naturels (les topos de faisceaux sur un espace topologique ou plus généralement une topologie de Grothendieck ou en particulier celui des ensembles simpliciaux, les topoï de réalisabilité comme le topos effectif) et qui correspondent à des objets qui avaient déjà été étudiés en maths avant qu'on se rende compte que ça forme des topoï, donc ça ne sort pas de nulle part. Et à un autre niveau, un topos c'est assez proche d'un modèle de la théorie de Zermelo intuitionniste (“IZ”), donc là aussi je comprends d'où cette notion sort.

Dans un topos ou dans un modèle de IZ, l'ensemble Ω des valeurs de vérité est l'ensemble des parties d'un singleton (et notamment deux valeurs de vérité qui s'impliquent l'une l'autre sont égales parce que chaque partie est contenue dans l'autre), une fonction X→Ω c'est pareil qu'une partie de X, et une fonction X→Y c'est pareil qu'un graphe fonctionnel dans X×Y, et l'axiome du choix unique vaut (dans IZ, c'est un théorème, au demeurant assez trivial parce que c'est essentiellement juste la définition du mot « fonction »). Des choses qui valent dans les maths “normales”, quoi.

Bref, j'ai une intuition de la sémantique qu'on essaie de capturer dans ce que je peux appeler les maths constructives (même si le terme est un peu flou). Ce ne sont pas des choses qui sorte d'un chapeau.

Donc si tu me demandes pourquoi l'axiome du choix unique ne me pose pas problème alors que l'axiome du choix si, ben la réponse est que l'axiome du choix unique, pour moi, c'est la définition de la notion de fonction, et/ou que c'est comme ça que les topoï voient les choses. Et manifestement ce n'est pas incompatible avec une interprétation constructive et algorithmique¹ des constructions, puisque le topos effectif est bien un topos.

S'agissant du fait que choix unique + tiers exclu implique l'existence de fonctions non calculables, Brouwer pensait clairement que c'était de la faute du tiers exclu (qu'il considérait comme un « principe d'omniscience »).

Après, je comprends qu'on puisse quand même vouloir affaiblir encore ces choses. Pourquoi pas : après tout, j'en veux à Bishop de faire des maths constructives avec l'axiome du choix dénombrable alors que ce dernier ne vaut pas dans un topos en général — peut-être que Bishop serait en droit de me demander quel est mon problème avec l'axiome du choix dénombrable. (Mais voilà, l'axiome du choix dénombrable je peux dire « il n'est pas valable dans le topos des faisceaux sur ℝ, et ce monde-là m'intéresse ».) Mais qu'est-ce qu'on essaie de capturer au juste, comme idée ? Quelle est l'intuition de ce qu'on cherche à faire analogue à ce qui a motivé Brouwer, Heyting et Bishop à proposer de faire des maths constructives ?

Au-delà des topoï, je crois que je comprends vaguement l'idée (même si je n'ai pas regardé trop les détails), pour ne pas avoir de proof irrelevance, d'identifier les propositions à des types tronqués, comme expliqué dans l'article “Propositions as [Types]” par Awodey et Bauer, et qui doit être ce qui sert en théorie homotopique des types : mais une fois que tu tronques, il y a proof irrelevance dans le type tronqué. (Si je comprends bien, cette façon de voir les propositions comme des types tronqués permet d'avoir à la fois le Σ des théories à la Martin-Löf, pour lequel l'axiome du choix est automatique, et le ∃ des théories logiques, en disant en gros que ‘∃’ c'est [Σ], et inversement, [P] en gros c'est ∃x:P.⊤. Je ne comprends pas les détails, mais j'ai au moins l'impression de comprendre l'intuition.) Manifestement, Coq ne fait pas ça : il y a une différence entre Type et Prop mais Prop n'est pas juste les troncatures des types de Type. Pareil, pour ce qui est de ‘->’ : je pourrais comprendre l'idée de dire qu'on va séparer les types fonctions et les types algorithmes (chaque algorithme détermine une fonction, mais on ne va pas postuler que toute fonction est définie par un algorithme, ni que deux algorithmes déterminant la même fonction soient égaux). Mais Coq ne fait pas ça non plus : il y a un seul ‘->’ et je ne sais pas ce qu'il est censé signifier.

Alors bien sûr tu peux me dire « Coq signifie exactement ce que les règle de Coq disent, ni plus ni moins ». (Je crois que c'est le genre d'attitude dont Girard se moque en parlant de brocolis : on invente des règles syntactiques, et on dit que la sémantique c'est juste tout ce qui vérifie ces règles.) D'accord, mais d'abord ces règles sont hyper difficiles à trouver (et en plus elles changent avec le temps : avant il n'y avait pas de SProp, maintenant il y en a), et elles ne sont pas les mêmes d'un système de preuve à un autre (Coq, Lean, Agda, HOL, Isabelle, je me perds rien que dans la liste de ces trucs), donc on ne peut pas sérieusement prétendre qu'elles tombent naturellement du ciel comme la notion de topos (qui est quand même au moins assez naturelle pour avoir été proposée par un géomètre algébriste qui voulait faire de la cohomologie étale et pour servir en logique — voilà un argument empirique pour se dire que c'est une notion assez naturelle). Les gens qui les choisissent doivent avoir une intuition sur ce qu'ils essaient de capturer avec ces règles (pour avoir choisi celles-ci plutôt que celles-là), mais ils se gardent bien de nous la dire, et je n'ai aucune idée de comment ils se la forgent. Pour moi les règles sortent juste d'un grand chapeau. Apparemment, dans certains de ces systèmes (certaines variantes d'Agda, si je comprends bien, ce qui est très incertain, peut-être Cubical Agda), l'axiome du choix unique vaut (je ne sais pas s'il est postulé ou s'il tombe des règles) : faut-il en déduire que l'intuition des gens qui ont imaginé ces systèmes est différente de celle de ceux qui ont imaginé Coq ? Que le chapeau n'est juste pas le même ?

Je comprends ton argument selon lequel le λ-calcul non typé avait une syntaxe avant d'avoir une sémantique (autre que la sémantique triviale — sauce aux brocolis — donnée par les termes modulo les règles de syntaxe…), mais quand même les règles du λ-calcul non typé, on voit qu'il n'y a pas énormément de décisions à faire pour les écrire, alors que le labyrinthe des règles de systèmes de typage prouve que, si, il y a plein de décisions à prendre (il n'y a pas trente-douze versions du λ-calcul non typé comme il y a trente-douze systèmes de types).

Et encore une chose : en maths constructives on peut déjà dire qu'il y a un labyrinthe de notions partiellement classiques (LPO, WLPO, LLPO, WLLPO, MP, etc.), donc que si je trouve ça intéressant je suis mal placé pour reprocher à Coq d'avoir un labyrinthe d'hypothèses (proof irrelevance, extensionalité propositionnelle, extensionalité fonctionnelle…). J'en conviens. Mais sur les hypothèses ajoutées aux maths constructives, on a justement toute une branche des mathématiques à rebours (cf. par exemple ce papier) qui cherche à cartographier le labyrinthe. Les gens qui font des systèmes de typage, non seulement j'ai l'impression qu'ils sortent les règles de leur chapeau, mais en plus je n'ai pas l'impression qu'ils cartographient le labyrinthe de ce que leurs propres règles permettent ou ne permettent pas de faire ! (Comment on sait, par exemple, que Coq ne prouve pas l'axiome du choix unique ? D'ailleurs, comment on sait que Coq ne prouve pas ⊥ ? C'est un théorème dont la preuve figure quelque part dans la littérature ?)

Voilà, désolé d'avoir ranté en mode « je n'y comprends rien », n'essaie surtout pas de répondre à tout ça dans les commentaires, en revanche ça peut peut-être te donner une idée des choses sur lesquelles ça m'intéresse d'en savoir plus, par exemple sous forme de billet de blog, si tu arrives à les comprendre de manière à potentiellement me déconfuser.

# Commentaire de Gro-Tsen (10 novembre 2024 à 21:38)

Mea culpa quand même pour la partie « je n'ai pas l'impression qu[e les théoriciens des types] cartographient le labyrinthe de ce que leurs propres règles permettent ou ne permettent pas de faire » dans l'avant-dernier paragraphe de mon précédent commentaire : tu m'as déjà signalé via Bluesky quelque chose qui répondait à ce point. Donc il faudrait sans doute regarder à quoi ressemblent les genres de modèles qu'ils utilisent pour répondre à ces questions, et ça donnera peut-être au moins une forme d'intuition sur ce que Prop est censé signifier ou autres questions existentielles (😉) du même type (😉).

# Commentaire de Jean Abou Samra (11 novembre 2024 à 01:34)

OK, je ne vais pas répondre à tout (surtout que je n'ai pas toutes les réponses). Je peux quand même donner des éléments sur des points faciles à clarifier.

je ne connais vraiment pas grand-chose à Coq, et ce n'est pas très intéressant à raconter vu que j'ai juste très peu de temps pour m'y intéresser (à vrai dire j'ai beaucoup de mal à lire les exemples, vu que je connais mal même la syntaxe, et aussi que les successions de tactiques sont hyper difficiles à suivre et que je sais à peine lancer le programme pour les essayer)

Je ne vais pas faire un billet là-dessus, mais si tu as des questions pratico-pratiques sur Coq, n'hésite à me @-mentionner (ou à le signaler sur Bluesky évidemment), que ce soit sur https://coq.zulipchat.com, sur https://coq.discourse.group ou sur https://proofassistants.stackexchange.com. Ou pour des choses simples à juste à m'envoyer un message par un quelconque moyen.

Je suis d'accord que c'est difficile simplement en lisant le code de comprendre une succession de tactiques. Il faut vraiment y aller pas-à-pas dans Proof General pour voir les hypothèses et le but à chaque étape.

Mais à un niveau plus large, et je vais plutôt ranter là-dessus, je ne sais juste pas ce que le Prop (ou le SProp, puisqu'il y a ça, maintenant) de Coq est censé représenter ou modéliser, intuitivement, ni, en fait, le signe ‘->’. (Par exemple, j'ai une certaine intuition sur le principe de Markov en maths constructives. Mais j'ai exactement zéro intuition sur la différence entre sa formulation comme forall p:nat->Prop, (forall n:nat, (p n)\/~(p n)) -> (~ forall n:nat, (p n)) -> (exists n:nat, ~(p n)) et comme forall p:nat->bool, (~ forall n:nat, (p n)=true) -> (exists n:nat, (p n)=false) an Coq.

Comme tu t'en es souvenu, il faudrait lire l'article que j'avais déniché (je ne l'ai pas fait), mais je peux donner au moins une intuition : remarque que la formulation

forall p : nat -> bool, (~forall n, p n = true) -> (exists n, p n = false)

est prouvablement équivalente à

forall p : nat -> Prop, (forall n, {p n} + {~p n}) -> (~forall n, p n) -> exists n, ~p n

(je peux écrire une preuve Coq propre si tu veux, il n'y a rien d'intelligent).

On voit ici que la seule différence avec la première formulation

forall p : nat -> Prop, (forall n, (p n) \/ (~p n)) -> (~forall n, p n) -> exists n, ~p n

est dans le (p n) \/ (~p n) qui est devenu un {p n} + {~p n}. Si on revient aux définitions, le \/ vient de

Inductive or (A B : Prop) : Prop :=
  | or_introl : A -> or A B
  | or_intror : B -> or A B.

alors que le { } + { } vient de

Inductive sumbool (A B : Prop) : Set :=
  | left : A -> sumbool A B
  | right : B -> sumbool A B.

À part le nommage et les notations, l'unique différence entre ces deux types est la sorte : or vit dans Prop (et n'est pas éliminable dans Type, il ne bénéficie pas de l'élimination des sous-singletons), alors que sumbool vit dans Set (càd le plus bas niveau de Type).

En gros, le MP avec { } + { } te dit : « Je veux bien faire une recherche non bornée grâce à la garantie qu'elle termine, mais seulement si ce que je teste est calculatoire ».

Pour comprendre mieux que cet agitage de mains en mode « preuves vs. calculs » la restriction sur l'élimination de Prop vers Type, il faut vraiment regarder les conséquences du paradoxe de Girard (nécessité de la prédicativité dans Type). Normalement, ça devrait être le prochain billet.

Comment on sait, par exemple, que Coq ne prouve pas l'axiome du choix unique ?

À vue de nez, un argument purement syntaxique sur la forme normale d'une preuve devrait marcher, non ? Je ne réfléchis pas plus, il faut que j'aille me coucher quand même.

D'ailleurs, comment on sait que Coq ne prouve pas ⊥ ? C'est un théorème dont la preuve figure quelque part dans la littérature ?

Non 😕

Pour le calcul des constructions pur, il y a ce papier : Strong Normalization for the Calculus of Constructions de Chris Casinghino, qui compare plusieurs preuves existantes.

Pour le calcul des constructions inductives, le mieux que j'ai trouvé est la thèse de Benjamin Werner. Comme on peut s'y attendre, c'est une preuve par candidats de réductibilité, sauf qu'évidemment tout est compliqué par les types inductifs.

Le souci, c'est que Coq, c'est plus que ça : il y a des let (et mine de rien ça complique énormément les choses, j'ai prévu d'en parler à un moment, mais l'équivalence habituelle entre let x := u in v et (fun x => v) u ne marche plus, un contre-exemple étant let A := True in (fun a : A => 42) I vs. (fun A => (fun a : A => 42) I) True), il y a des types co-inductifs, il y a SProp, la hiérarchie avec Prop imprédicatifs et tous les univers prédicatifs au-dessus n'a pas l'air d'être la même que dans la thèse de Werner, et contrairement à la thèse de Werner il n'y a pas d'η-réduction mais par contre il y a une η-expansion (oui) (à rapprocher, je crois, de la mise sous forme β-normale η-longue en λ-calcul simplement typé, cf. ici et là), et puis il y a aussi un machin « hautement expérimental » de règles de réécritures à la Dedukti / λΠ-calcul modulo théorie (ce que font Dowek & co. au LMF), et probablement d'autres choses encore… J'ai l'impression qu'on comprend à peu près chacune de ces extensions individuellement, sauf qu'il n'y a pas encore de preuve qui unifie tout.

Et pour finir sur une dernière différence, qui est une merde de mammouth en travers d'une preuve de cohérence, Coq (contrairement à Lean) a le pattern matching et les définitions récursives syntaxiquement bien fondées (Fixpoint / fix) comme primitives, plutôt que de les compiler avec les éliminateurs générés pour les inductifs. Et ce truc est mal compris, assez ad hoc et pas formalisé du tout, cf. ceci.

Il y a le projet MetaCoq, qui vise à formaliser Coq en Coq, et qui apparemment a bien avancé (c'est un bouzin de qqch comme 300 000 lignes de code…), mais ils n'ont le théorème de cohérence que sous l'hypothèse que la normalisation forte est vérifiée. La normalisation forte n'est pas encore prouvée, et j'ai cru comprendre que les fix étaient une grosse partie du problème.

# Commentaire de Jean Abou Samra (11 novembre 2024 à 12:09)

(je peux écrire une preuve Coq propre si tu veux, il n'y a rien d'intelligent)

En fait je l'ai fait, pour m'assurer que je n'étais pas en train de raconter des bêtises, donc voilà :

Require Import Setoid.

Definition MP_bool :=
  forall P : nat -> bool,
    (~forall n, P n = true) ->
    exists n, P n = false.

Definition MP_Prop_alt :=
  forall P : nat -> Prop,
    (forall n, {P n} + {~P n}) ->
    (~forall n, P n) ->
    exists n, ~P n.

Remark rmk1 : MP_bool <-> MP_Prop_alt.
Proof.
  split; intros MP.
  - intros P H_decidable H_termination.
    set (f n := match H_decidable n with left _ => true | right _ => false end).
    assert (RW : forall n, P n <-> f n = true). {
      intros n. unfold f. destruct (H_decidable n) as [Pn | notPn].
      - tauto.
      - split.
        + tauto.
        + discriminate.
    }
    setoid_rewrite RW in H_termination.
    specialize (MP f H_termination). destruct MP as [n Hn].
    exists n. rewrite RW. rewrite Hn. discriminate.
  - intros P H_termination.
    set (f n := P n = true).
    assert (H_decidable : forall n, {f n} + {~f n}). {
      intros n. unfold f. destruct (P n).
      - left. reflexivity.
      - right. discriminate.
    }
    specialize (MP f H_decidable H_termination). destruct MP as [n Hn].
    exists n. unfold f in Hn. destruct (P n); tauto.
Qed.

# Commentaire de Gro-Tsen (11 novembre 2024 à 12:56)

Le problème est que tu as expliqué la version de MP avec ‘+’ en lui donnant l'explication intuitive que je donne, moi, à celle avec ‘∨’ (dans un topos les deux sont équivalentes, mais on le décrit informellement avec des suites booléennes et en gros comme tu l'as dit). On en revient toujours au même:quel est le sens de cette distinction entre ‘+’ et ‘∨’? Qu'est-ce que Coq fait de différent de la logique des topoï pour que cette distinction existe, et dans quel but le font-ils? (Est-ce d'ailleurs le même problème qu'avec le choix unique ou est-ce une question différente?) L'idée intuitive que j'ai (et Brouwer aussi, je crois) du p∨q constructif c'est “p ou q est vrai et on sait lequel”, tandis que “p ou q est vrai et on ne sait pas lequel” serait ¬(¬p∧¬q). Mais Coq a un p+q qui semble correspondre à mon idée intuitive de p∨q, mais il a AUSSI un p∨q qui n'est pas ¬(¬p∧¬q). Donc maintenant je voudrais une explication de cette distinction triple (et il y a peut-être plus que 3 trucs naturels, d'ailleurs!), et à quoi ça sert d'avoir un ‘∨’ régi par la logique intuitionniste si la disjonction vraiment constructive c'est en fait le ‘+’. 🤔 (C'est d'autant plus mystérieux que la distinction entre ‘+’ et ‘∨’ de Coq n'a pas de sens au niveau purement propositionnel. Donc le ‘∨’ de Coq ✳︎ne peut pas✳︎ être “l'un des deux vaut mais je ne sais pas lequel” car ce dernier devrait valider les tautologies propositionnelles classiques.)

Je ne m'attends évidemment pas à ce que tu aies une réponse. Mais je veux bien savoir si tu comprends et partages ma perplexité (voire, mon agacement). J'ai l'impression qu'il y a un truc central très simple que je ne saisis pas mais je ne sais même pas formuler cette question centrale.

# Commentaire de Jean Abou Samra (11 novembre 2024 à 16:05)

Bon, il faudra vraiment que j'écrive quelque part une liste des raisons pour lesquelles on a envie de distinguer Prop de Type.

Ce sera plus facile quand j'aurai expliqué le paradoxe de Girard. J'essaierai à ce moment-là de trouver un exemple intéressant où le MP dans Prop peut servir et celui de Type ne peut pas (forcément pour cause de prédicativité), ce sera plus concret.

Remarque : Le + / {} + {} est à ∨ / \/ exactement ce que Σ / { ... | ... } est à ∃ / exists. (Je ne sais pas si c'était clair pour toi, je le prenais comme implicitement évident mais j'aurais peut-être dû le préciser.)

Pour répondre à ta dernière question, je partage en partie ta perplexité, mais je pense que je commence à avoir une certaine intuition, et surtout, en fait, ça va peut-être te surprendre mais je trouve ça plus intuitif que les topos. C'est contre-intuitif pour moi que l'axiome du choix unique soit vrai dans tout topos alors que ce n'est pas le cas de l'axiome du choix : je comprends bien que c'est plus ou moins la définition d'une fonction dans ce cadre à cause d'un codage pseudo-ensembliste, mais la dissymétrie reste là. (L'idéal étant, dans mon esprit, d'avoir une notion unifiée de fonction qui marche à la fois pour la notion mathématique et, via Curry-Howard, pour les preuves de propositions universellement quantifiées. C'est ce qu'essaie de faire Coq, l'effet malheureux étant de casser l'extensionnalité fonctionnelle et le choix unique. Mais l'élégance d'identifier entièrement les deux garde quand même de l'attrait.)

# Commentaire de Informatheux (12 novembre 2024 à 18:48)

Je crois qu'il peut être utile de rajouter à la discussion le fait que l'axiome du choix dans sa forme constructive, et a fortiori le choix unique, sont "souvent" valides en Coq. C'est quand on mélange les différents univers que ça peut poser problème : avoir un univers prédicatif est important, puisque sans ça la force logique est plus faible que l'arithmétique du second ordre, cf cette réponse de Loïc Pujet, mais ça n'interagit pas aussi bien qu'on le voudrait avec la hiérarchie prédicative.

Pour l'exemple, si j'ai un type A, un prédicat P : A -> Type, et que pour tout a : A il existe p : P a tel que Q a p, cet "il existe" étant pris dans Type, alors il existe (dans Type) une fonction qui à chaque a va associer un élément de P a tel que Q a (f a).

Du coup, voir A -> B (et même forall (a : A), P a) comme le type des algorithmes qui prennent un A et renvoie un B me semble tout à fait correct. Comme la théorie est intensionnelle, je trouve qu'on a plutôt les algorithmes que les fonctions au sens mathématiques (mais ça peut se changer en ajoutant l'axiome d'extensionnalité des fonctions).

C'est par contre quelque chose qui diffèrent pas mal entre les topos et les diverses théories des types : en général les théories des types sont assez intensionnelles, et quand on contourne ça, c'est compliqué. J'ai l'impression que soit c'est avec des axiomes qui cassent les calculs (SProp a des principes d'éliminations encore plus contraignants que Prop) ou la décidabilité (cf. Lean), HoTT ne calcule pas sur l'univalence (Cubical si, mais j'ai du mal à comprendre)

A contrario, les topos sont très extensionnels : tout est défini à partir de constructions universelles qui assurent l'unique existence à unique isomorphisme près, mais c'est pas très pratique pour calculer ; par exemple, en théorie des ensembles, c'est il me semble impossible de définir le foncteur PSh(C) -> Sh(C) sans l'axiome du choix.

Laisser un commentaire

Nom ou pseudo (obligatoire) :

Email (facultatif, ne sera montré qu'à l'auteur) :

Page Web (facultatif) :

Mémoriser ces informations dans ce navigateur pour mon prochain commentaire

Copiez le code suivant (obligatoire, mesure anti-spam) : 3551850194

Commentaire (aide Markdown, aide KaTeX) :