Les subtilités de Coq, épisode 2 : sur l'axiome du choix

22 novembre 2024 ⋅ Retour à l'accueil du blog

Je continue ma série commencée au billet précédent sur Coq et plus généralement la théorie des types, avec quelques remarques sur l'axiome du choix, ses variantes, sa constructivité ou non-constructivité, et les liens à faire avec la distinction entre Prop et Type. Je vais raconter des choses somme toute assez simples, mais qui ne sont expliquées de manière cohérente à peu près nulle part, donc n'ayons pas peur des choses simples.

Pour les théoriciens des topos élémentaires, la situation se décrit en peu de mots. Dans la logique interne d'un topos,

• Les différentes formulations que l'on peut raisonnablement imaginer pour l'axiome du choix sont toutes équivalentes.
• L'axiome du choix implique le tiers exclu, c'est le théorème de Diaconescu.
• L'axiome du choix unique, la variante qui affirme que toute relation fonctionnelle peut se réifier en une fonction, est vrai.

En théorie des types… on perd ces trois points à la fois, et tout devient plus compliqué, pour diverses raisons. Les principaux coupables sont l'absence d'extensionnalité fonctionnelle, l'absence d'extensionnalité propositionnelle, l'absence d'indiscernabilité des preuves [j'adopte cette expression comme traduction de proof irrelevance], et aussi la distinction entre Prop et Type, qui s'accompagne de l'interdiction d'éliminer de Prop vers Type (sauf dans les conditions particulières détaillées dans le billet précédent).

On verra que certaines formes de l'axiome du choix seront prouvables — mais pas l'axiome du choix unique comme dans les topos. La distinction qui va intervenir est plutôt celle entre le $∃$ et le $Σ$, entre entre l'existence exists x, P x dans l'univers imprédicatif Prop et l'existence {x | P x} dans Type à la Martin-Löf. En fait, on remarque une énorme différence entre Prop et Type puisque l'axiome du choix « dans Type » est prouvable, alors que l'axiome du choix « dans Prop » non seulement ne l'est pas, mais impliqué carrément le tiers exclu, modulo d'autres axiomes largement considérés comme raisonnables. Je trouve ceci, à première vue, assez surprenant, et je pense qu'il vaut la peine de s'y pencher de plus près pour comprendre comment exactement l'axiome du choix dans Prop introduit de la non-constructivité d'une manière qui n'est pas possible dans Type.

Les différentes formes de l'axiome du choix

Naturellement, pour fixer le décor, je dois commencer par discuter des différentes variantes de l'axiome du choix et des raisons pour lesquelles elles sont ou ne sont pas équivalentes. Malheureusement, il en existe énormément dans le cadre de la théorie des types. Le module Logic.ChoiceFacts de la bibliothèque standard de Coq en liste des dizaines. Je ne vais pas en discuter exhaustivement (je renvoie à ce module et son code pour plus de précisions), mais seulement retenir celles qui me paraissent les plus importantes (et comme je ne suis pas spécialiste, j'avoue que ce choix est un peu pifométrique).

Je ne crois pas que la terminologie soit standardisée. Les noms de ces axiomes sont en partie sortis de mon chapeau, même si j'ai essayé de ne pas trop dévier de Logic.ChoiceFacts.

Par relation surjective, j'entends une relation $R$ entre deux ensembles $X$ et $Y$ qui vérifie $∀ x, ∃ y, R(x, y)$, et par relation fonctionnelle, une relation qui vérifie $∀ x, ∃! y, R(x, y)$.

1. L'axiome du choix relationnel affirme que toute relation surjective possède une sous-relation qui est fonctionnelle :

$$∀ X Y, ∀ R : X × Y → \text{Prop}, (∀ x, ∃ y, R(x, y)) ⇒ ∃ R' : X × Y → \text{Prop}, (∀ x y, R'(x, y) ⇒ R(x, y)) ∧ (∀ x, ∃! y, R'(x, y))$$

Axiom relational_choice :
  forall (X Y : Type) (R : X -> Y -> Prop),
    (forall x, exists y, R x y) ->
    exists R' : X -> Y -> Prop,
      (forall x y, R' x y -> R x y) /\
      (forall x, exists! y, R' x y).

2. L'axiome du choix relationnel-fonctionnel affirme que pour toute relation surjective, il existe une fonction dont le graphe est inclus dans la relation :

$$∀ X Y, ∀ R : X × Y → \text{Prop}, (∀ x, ∃ y, R(x, y)) ⇒ ∃ f : X → Y, (∀ x, R(x, f(x)))$$

Axiom relational_functional_choice :
  forall (X Y : Type) (R : X -> Y -> Prop),
    (forall x, exists y, R x y) ->
    exists f : X -> Y, forall x, R x (f x).

3. L'axiome du choix fonctionnel affirme que toute surjection admet une section :

$$∀ X Y, ∀ f : Y → X, (∀ x, ∃ y, x = f(y)) ⇒ ∃ g : X → Y, ∀ x, x = f(g(x))$$

(j'ai inversé le sens habituel des flèches pour souligner le parallèle avec les précédents).

Axiom functional_choice :
  forall (X Y : Type) (f : Y -> X),
    (forall x, exists y, x = f y) ->
    exists g : X -> Y, forall x, x = f (g x).

4. L'axiome du choix unique affirme que toute relation fonctionnelle est le graphe d'une fonction :

$$∀ X Y, ∀ R : X × Y → \text{Prop}, (∀ x, ∃! y, R(x, y)) ⇒ ∃ f : X → Y, (∀ x, R(x, f(x)))$$

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

5. L'axiome de description constructive indéfinie est, schématiquement, « ∃ ⇒ Σ », soit un transport de l'existence de Prop vers Type :

$$∀ X, ∀ P : X → \text{Prop}, (∃ x, P(x)) ⇒ (Σ x, P(x))$$

Axiom constructive_indefinite_description :
  forall (X : Type) (P : X -> Prop),
    (exists x, P x) -> {x | P x}.

6. L'axiome de description constructive définie est l'équivalent pour l'existence unique ∃! seulement :

$$∀ X, ∀ P : X → \text{Prop}, (∃! x, P(x)) ⇒ (Σ x, P(x))$$

Axiom constructive_definite_description :
  forall (X :Type) (P : X -> Prop),
    (exists! x, P x) -> {x | P x}.

7. L'axiome de déplacement de troncature permet de commuter les forall et les inhabited :

$$∀ X, ∀ (Y_x)_{x : X}, (∀ x, ∃ y : Y_x, ⊤) ⇒ (∃ f : (∀ x, Y_x), ⊤)$$

Axiom truncation_shift :
  forall (X : Type) (Y : X -> Type),
    (forall x, inhabited (Y x)) ->
    inhabited (forall x, Y x).

8. L'axiome du choix global est le plus simple et affirme que de tout type habité (il existe, ∃, un élément) on peut obtenir (Σ) un élément, ce qui revient là encore à traverser la frontière normalement interdite entre Prop et Type :

$$∀ X, (∃ x : X, ⊤) ⇒ (Σ x : X, ⊤)$$

Axiom global_choice : forall (X : Type), inhabited X -> X.

9. L'axiome du choix global unique est l'équivalent de l'axiome du choix global,

$$∀ X, (∃! x : X, ⊤) ⇒ (Σ x : X, ⊤)$$

Inductive inhabited_unique (X : Type) : Prop :=
| inhabits_unique : forall (x : X), (forall y : X, y = x) -> inhabited_unique X.

Axiom global_unique_choice : forall (X : Type), inhabited_unique X -> X.

Remarque sur la terminologie « global »

Évidemment, quelques commentaires s'imposent. Je commence par une remarque sur le sens de « global » dans ce contexte. Traditionnellement, en théorie des ensembles, l'axiome du choix global ne peut pas s'exprimer sous forme d'une proposition, et il n'est appelé « axiome » que par abus de langage. Ce qu'apporte le choix global par rapport au choix simple est l'uniformité : non seulement on peut choisir des éléments des ensembles non-vides, mais on peut le faire en gardant le même choix d'élément pour chaque ensemble. Il se « postule », typiquement, en rajoutant un symbole de fonction $C$ dans la théorie, accompagné de l'axiome $∀ X, X ≠ ∅ ⇒ C(X) ∈ X$. Or, ici, comme les propositions ne sont pas séparées des fonctions, on peut parfaitement « postuler une fonction », et c'est ce que fait l'axiome global_choice proposé ci-dessus. On peut être surpris que j'aie donné à côté une formule logique en l'appelant « axiome du choix global » : il faut simplement se rappeler que cet axiome n'est pas une proposition, et d'ailleurs on peut vérifier que son type n'est pas dans la sorte Prop mais bien dans Type. Cette formulation est donc bien « la bonne manière » d'encoder l'équivalent de l'axiome du choix global de la théorie des ensembles.

(J'aurais peut-être dû noter $Π$ au lieu de $∀$ dans la formule, mais c'est simplement psychologique. Il n'y a qu'un quantificateur universel en Coq et dans toutes les théories des types que je connais, au contraire de l'existence qui peut être séparée en $∃$ et $Σ$. Ce sont les sortes à l'intérieur du $∀$ qui déterminent la sorte du $∀$ entier.)

Mais il faut également réaliser que les autres variantes ont aussi, d'une certaine façon, un caractère « global ». Prenons par exemple le choix relationnel, qui, lui, est purement propositionnel. En théorie des ensembles, si on applique deux fois l'axiome du choix relationnel à la même relation, on ne peut pas conclure a priori que les deux sous-relations fonctionnelles obtenues sont égales : des applications différentes de l'axiome du choix donnent potentiellement des résultats différents (on pourrait presque appeler cela du non-déterminisme). En théorie des types, ajouter cet axiome revient à ajouter un terme dont on postule qu'il a un certain type. Si on l'applique à des endroits différents aux mêmes objets, les termes obtenus sont structurellement identiques, donc définitionnellement égaux, donc on peut les prouver égaux propositionnellement (avec reflexivity en Coq).

Je n'ai pas d'exemple d'application en tête, mais on peut imaginer la situation suivante : dans une preuve, on utilise l'axiome du choix relationnel sur une relation $R$ entre $X$ et $Y$, et par ailleurs sur une relation $S$ entre $Z$ et $T$, puis dans un certain sous-cas, on se rend compte que $R = S, X = Z, Y = T$. On peut alors en déduire que les relations extraites sont les mêmes… à condition que les preuves des prémisses $∀ x, ∃ y, R(x, y)$ et $∀ z, ∃ t, S(z, t)$ soient les mêmes. Remarquer au passage que ce problème se pose aussi avec l'axiome du choix global, puisque pour conclure global_choice X P = global_choice X Q, il faut P = Q (où P, Q : inhabited X). Bien sûr, si on travaille sous l'axiome d'indiscernabilité des preuves, alors la question ne se pose plus.

Liens entre les différentes variantes

Discutons maintenant des implications et non-implications qui existent entre toutes ces variantes. Ceci est légèrement fastidieux et pas spécialement passionnant, mais je trouve utile de le faire pour explorer le paysage, parce que de même qu'il est facile de faire accidentellement un raisonnement classique quand on se familiarise avec les maths constructives, je trouve qu'il est facile de faire accidentellement un raisonnement qui s'appuie sur l'extensionnalité fonctionnelle ou propositionnelle en théorie des types (en tous cas, je n'avais pas les idées claires sur ce qui allait passer ou pas en théorie des types avant d'écrire ce billet, donc me forcer à faire tous ces petits exercices idiots en Coq m'aura au moins été utile à moi).

Il est clair que l'axiome du choix relationnel-fonctionnel implique l'axiome du choix relationnel, car si on peut extraire d'une relation surjective une function, le graphe de cette fonction est une relation fonctionnelle incluse dans la relation surjective de départ. Ce qui empêche de prouver l'autre implication est l'impossibilité de réifier nativement une relation fonctionnelle en une fonction. Or c'est justement ce que propose l'axiome du choix unique. Par ailleurs, il est également clair que l'axiome du choix relationnel-fonctionnel implique l'axiome du choix unique (si on peut extraire une fonction d'une relation surjective, on peut en particulier extraire une fonction d'une relation fonctionnelle). Au total, le résultat est donc : choix relationnel-fonctionnel ⇔ choix relationnel ∧ choix unique.

Et l'axiome du choix fonctionnel ? C'est le cas particulier de l'axiome du choix relationnel-fonctionnel restreint aux relations qui sont l'inverse du graphe d'une fonction (en particulier ces relations doivent être « fonctionnelles à droite », c'est-à-dire $∀ y, ∃! x, R(x, y)$). On se rend compte que ce cas particulier permet de retrouver le cas général, soit choix relationnel-fonctionnel ⇔ choix fonctionnel. En effet, dans le cas général avec une relation R : X -> Y -> Prop telle que forall x, exists y, R x y, on peut artificiellement « rendre cette relation fonctionnelle à droite en séparant les y associés à un même x », en posant Z le type {x & {y | R x y}} des couples de deux éléments reliés par R. En considérant la fonction qui envoie un tel triplet de x, y et une preuve sur x, on constate que l'axiome du choix fonctionnel s'applique et le reste ne pose plus de difficulté.

Que penser du déplacement de troncature ? On constate sans trop de mal qu'il implique le choix relationnel-fonctionnel : en réécrivant forall x, exists y, R x y en forall x, inhabited {y | R x y}, on peut appliquer le déplacement de troncature pour obtenir inhabited (forall x, {y | R x y}), et le résultat en découle. La réciproque saute moins aux yeux, mais elle néanmoins vraie, avec une petite transformation semblable au paragraphe précédent : l'idée sous-jacente est de transformer l'hypothèse avec un type dépendant forall x, inhabited (Y x) en une hypothèse sans dépendance forall x, exists z, R x z, où le type de z va être l'union disjointe de tous les Y x. On a donc choix relationnel-fonctionnel ⇔ déplacement de troncature.

Sans grande surprise, l'axiome du choix global implique toutes les autres variantes présentées ici. On peut aussi remarquer immédiatement que l'axiome de description constructive indéfinie est en fait équivalent au choix global, en posant simplement P x := True. Si je l'ai tout de même présenté à part, c'est pour pouvoir souligner que l'axiome de description constructive définie n'est pas équivalent a priori à l'axiome du choix global unique. On aurait pourtant l'impression d'un parallèle parfait : on passe du choix global au choix global unique en rajoutant juste un $!$ sur un $∃$, et de même pour passer de la description constructive indéfinie à la description constructive définie. On vérifie que l'axiome de description constructive définie implique le choix global unique, à nouveau en posant essentiellement P x := True. Si la réciproque n'est pas vraie a priori, c'est parce que pour donner un habitant de {x | P x} à l'aide du choix global unique, il faut que ce type soit un singleton, or l'hypothèse exists! x, P x n'y suffit pas car elle donne l'unicité du x mais pas l'unicité de la preuve de P x — il faut donc rajouter l'indiscernabilité des preuves pour s'en sortir.

Pour exactement la même raison, on ne peut pas passer simplement du choix global unique au choix unique, parce qu'à nouveau, on a besoin de l'indiscernabilité des preuves pour que le type dont on extrait un élément soit vraiment un singleton.

Voici donc un schéma (vite et mal fait) qui résume des diverses implications que j'ai données :

Et voici les preuves proprement formalisées de toutes ces implications :

Definition Relational_choice :=
  forall (X Y : Type) (R : X -> Y -> Prop),
    (forall x, exists y, R x y) ->
    exists R' : X -> Y -> Prop,
      (forall x y, R' x y -> R x y) /\
      (forall x, exists! y, R' x y).

Definition Relational_functional_choice :=
  forall (X Y : Type) (R : X -> Y -> Prop),
    (forall x, exists y, R x y) ->
    exists f : X -> Y, forall x, R x (f x).

Definition Functional_choice :=
  forall (X Y : Type) (f : Y -> X),
    (forall x, exists y, x = f y) ->
    exists g : X -> Y, forall x, x = f (g x).

Definition Unique_choice :=
  forall (X Y : Type) (R : X -> Y -> Prop),
    (forall x, exists! y, R x y) ->
    exists f : X -> Y, forall x, R x (f x).

Definition Constructive_indefinite_description :=
  forall (X : Type) (P : X -> Prop),
    (exists x, P x) -> {x | P x}.

Definition Constructive_definite_description :=
  forall (X :Type) (P : X -> Prop),
    (exists! x, P x) -> {x | P x}.

Definition Truncation_shift :=
  forall (X : Type) (Y : X -> Type),
    (forall x, inhabited (Y x)) ->
    inhabited (forall x, Y x).

Definition Global_choice := forall (X : Type), inhabited X -> X.

Inductive inhabited_unique (X : Type) : Prop :=
| inhabits_unique : forall (x : X), (forall y : X, y = x) -> inhabited_unique X.

Definition Global_unique_choice := forall (X : Type), inhabited_unique X -> X.

Definition Proof_irrelevance := forall (P : Prop) (p1 p2 : P), p1 = p2.


Goal Global_choice -> Truncation_shift.
Proof.
  intros global_choice X Y H. constructor. intros x.
  apply global_choice. apply H.
Qed.

Goal Truncation_shift -> Relational_functional_choice.
Proof.
  intros truncation_shift X Y R H.
  set (Inh := fun x => exists_to_inhabited_sig (H x)).
  destruct (truncation_shift X (fun x => {y | R x y}) Inh) as [F].
  set (f := fun x => let (y, _) := F x in y). exists f.
  intros x. unfold f. destruct (F x) as [y Hy]. apply Hy.
Qed.

Goal Relational_functional_choice -> Truncation_shift.
Proof.
  intros relational_functional_choice X Y H.
  set (Z := {x & Y x}).
  set (R := fun (x : X) (z : Z) => let (x2, y) := z in x = x2).
  assert (H' : forall x, exists z, R x z). {
    intros x. destruct (H x) as [y].
    set (z := existT Y x y : Z).
    exists z. simpl. reflexivity.
  }
  destruct (relational_functional_choice X Z R H') as [f Hf].
  constructor. intros x. specialize (Hf x). destruct (f x) as [y Hy].
  simpl in Hf. rewrite <- Hf in Hy. exact Hy.
Qed.

Goal Relational_functional_choice <-> Relational_choice /\ Unique_choice.
Proof.
  split.
  - intros relational_functional_choice. split.
    + intros X Y R H.
      destruct (relational_functional_choice X Y R H) as [f Hf].
      exists (fun x y => y = f x). split.
      * intros x y E. subst y. apply Hf.
      * firstorder.
    + intros X Y R H.
      assert (H' : forall x, exists y, R x y) by firstorder.
      apply (relational_functional_choice X Y R H').
  - intros [relational_choice unique_choice] X Y R H.
    destruct (relational_choice X Y R H) as [R' [R'_subrelation R'_functional]].
    destruct (unique_choice X Y R' R'_functional) as [f Hf].
    exists f. intros x. apply R'_subrelation. apply Hf.
Qed.

Goal Relational_functional_choice -> Functional_choice.
Proof.
  intros relational_functional_choice X Y f H.
  apply (relational_functional_choice X Y (fun x y => x = f y) H).
Qed.

Goal Functional_choice -> Relational_functional_choice.
Proof.
  intros functional_choice X Y R H.
  set (Z := {x & {y | R x y}}).
  set (f := fun (z : Z) => let (x, y) := z in x).
  assert (H' : forall x, exists z, x = f z). {
    intros x. destruct (H x) as [y Hy].
    exists (existT _ x (exist _ y Hy)).
    simpl. reflexivity.
  }
  destruct (functional_choice X Z f H') as [g Hg].
  exists (fun x => let (_, s) := g x in let (y, _) := s in y).
  intros x. specialize (Hg x). destruct (g x) as [x2 [y Hy]].
  simpl in Hg. subst x2. apply Hy.
Qed.

Goal Global_choice -> Constructive_indefinite_description.
Proof.
  intros global_choice X P H. apply global_choice.
  destruct H as [x Hx]. constructor. exists x. apply Hx.
Qed.

Goal Constructive_indefinite_description -> Global_choice.
Proof.
  intros constructive_indefinite_description X H.
  assert (H' : exists x : X, True). { destruct H as [x]. exists x. constructor. }
  destruct (constructive_indefinite_description X (fun _ => True) H') as [x _].
  exact x.
Qed.

Goal Global_choice -> Constructive_definite_description.
Proof.
  intros global_choice X P H. apply global_choice.
  destruct H as [x [x_works x_unique]].
  constructor. exists x. apply x_works.
Qed.

Goal Constructive_definite_description -> Global_unique_choice.
Proof.
  intros constructive_definite_description X H.
  assert (H' : exists! x : X, True). {
    destruct H as [x Hx]. exists x. split.
    - constructor.
    - intros x' _. symmetry. apply Hx.
  }
  destruct (constructive_definite_description X (fun _ => True) H') as [x _].
  exact x.
Qed.

Goal Proof_irrelevance -> Global_unique_choice -> Constructive_definite_description.
Proof.
  intros proof_irrelevance global_unique_choice X P H.
  apply global_unique_choice. destruct H as [x [x_works x_unique]].
  set (inhabitant := exist P x x_works). exists inhabitant.
  intros [y y_works].
  assert (x = y). { apply x_unique. apply y_works. } subst y.
  assert (x_works = y_works). { apply proof_irrelevance. } subst y_works.
  reflexivity.
Qed.

Goal Proof_irrelevance -> Global_unique_choice -> Unique_choice.
Proof.
  intros proof_irrelevance global_unique_choice X Y R H.
  set (Z := fun x => {y | R x y}).
  assert (H' : forall x, inhabited_unique (Z x)). {
    intros x. destruct (H x) as [y [y_works y_unique]].
    exists (exist _ y y_works). intros [y2 y2_works].
    assert (y = y2). { apply y_unique. apply y2_works. } subst y2.
    assert (y_works = y2_works). { apply proof_irrelevance. } subst y2_works.
    reflexivity.
  }
  set (F := fun x => global_unique_choice (Z x) (H' x)).
  exists (fun x => let (y, _) := F x in y).
  intros x. destruct (F x) as [y y_works]. apply y_works.
Qed.

J'espère ne pas avoir oublié d'implication possible entre les variantes que j'ai présentées. Quoi qu'il en soit, je ne vais pas faire une liste à la Prévert avec toutes les variantes que je peux imaginer (encore une fois, il y en a d'autres dans Logic.ChoiceFacts : des variantes « gardées », « omniscientes », …).

Que conclure ? Quelles sont les variantes réellement intéressantes ?

Évidemment, l'axiome du choix global est la version toute-puissante. De manière très pragmatique, il faut tout de même noter qu'il casse l'extraction, en transgressant la frontière entre Prop et Type. (Par exemple, avec le tiers exclu, on prouve que toute machine de Turing M termine ou diverge, or M_termine \/ M_diverge implique inhabits ({M_termine} + {M_diverge}), et le choix global permet d'en tirer {M_termine} + {M_diverge} : ainsi on peut définir une fonction nat -> bool non-calculable, donc automatiquement impossible à extraire.)

Au contraire, les trois axiomes équivalents de choix relationnel-fonctionnel, choix fonctionnel et déplacement de la troncature sont compatibles à l'extraction, puisqu'ils renvoient du Prop ; ils correspondent aussi aux formulations les plus habituelles de l'axiome du choix en théorie des ensembles, et je suis tenté de conclure que c'est « la bonne » variante de l'axiome du choix si on veut conserver l'extraction. Le choix relationnel me semble moins intéressant, mais c'est peut-être simplement parce que je sais pas quel genre de modèles pourraient le vérifier sans vérifier le choix unique. Pour avoir une meilleure idée, il serait intéressant d'examiner le rapport avec le principe du bon ordre. Je n'ai pas le courage de le faire maintenant, mais si vous le faites, n'hésitez pas à partager vos conclusions dans les commentaires !

Au passage, je trouve que la formulation comme déplacement de troncature donne une intuition qui est légèrement différente de l'intuition standard « on fixe un choix d'un élément dans chaque ensemble », bien qu'elle soit très semblable à la formulation usuelle de la théorie des ensembles « un produit est habité si chacun de ses éléments est habité ». Je décrirais cette intuition comme « on s'autorise une transgression pour transporter une valeur de Prop vers Type, mais tout ceci n'est utilisé que pour revenir dans Prop, donc on se fait pardonner ». Remarquer l'analogie avec le déplacement de la double négation, un axiome possible en maths constructives qui n'est pas propre à la théorie des types et qui s'écrit $(∀ x, ¬¬P(x)) ⇒ (¬¬∀ x, P(x))$, soit un déplacement de $¬¬$ à l'extérieur d'un $∀$, là où le déplacement de la troncature est exactement la même chose pour déplacer un inhabits.

Je dois aussi mentionner que je n'ai pas de preuve que le choix relationnel n'implique pas le choix unique (donc le déplacement de troncature et les deux autres équivalents), même si j'en suis très convaincu. Il faudrait sans doute construire des modèles, or il n'existe pas de construction complète et formalisée d'un modèle de Coq, puisque ceci prouverait la cohérence, qui est l'objet de travaux en ce moment (cf. ce commentaire sur le billet précédent, et aussi celui-ci pour une perspective plus humoristique). Il existe, par contre, des modèles de versions simplifiées (si je comprends bien, des variantes sans co-induction, avec seulement des éliminateurs au lieu d'une guard condition, et ce genre de simplifications), mais je ne me suis pas penché dessus. (En revanche, j'ai donné plus haut une « preuve » que le déplacement de troncature n'implique pas le choix global : il faudrait formaliser l'effacement de Prop qu'opère l'extraction pour que ce soit une vraie preuve, mais c'est au moins une justification convaincante. C'est la seule séparation que je sais donner : je ne sais pas non plus prouver que le choix unique global n'implique pas le choix unique, par exemple.)

Je m'arrête là pour cette partie, mais je suis sûr qu'il y aurait des choses beaucoup plus intéressantes à dire en explorant la littérature, simplement je trouve un peu difficile de s'y retrouver. Si vous vous y connaissez, les précisions seront bienvenues.

Lien avec le tiers exclu : le théorème de Diaconescu

Je passe au deuxième sujet de ce billet (plus intéressant), le lien entre l'axiome du choix et le tiers exclu. Dans les topos, comme mentionné en introduction, l'axiome du choix implique le tiers exclu. Avant de continuer, je rappelle la preuve usuelle de ce résultat qui s'appelle le théorème de Diaconescu.

Preuve : Supposons l'axiome du choix. Soit $P$ une proposition. Posons $U := \{b ∈ \{⊥, ⊤\} \ | \ b = ⊥ ∨ P\}$ et $V := \{b ∈ \{⊥, ⊤\} \ | \ b = ⊤ ∨ P\}$. Les deux ensembles $U$ et $V$ sont clairement habités (le premier par $⊥$, le deuxième par $⊤$), donc il existe une fonction de choix pour l'ensemble $\{U, V\}$, c'est-à-dire une fonction $f : \{U, V\} → \{⊥, ⊤\}$ telle que $∀ W ∈ \{U, V\}, f(W) ∈ W$ (attention, la notation $\{U, V\}$ n'affirme pas que $U$ et $V$ sont distincts, et c'est fondamental). Si $f(U) = ⊤$, alors $⊤ ∈ U := \{b ∈ \{⊥, ⊤\} \ | \ b = ⊥ ∨ P\}$, donc $P$. De même, si $f(V) = ⊥$, alors $P$. Reste le cas $f(U) = ⊥, f(V) = ⊤$. Dans ce cas, en supposant $P$, on a $U = V = \{⊥, ⊤\}$, absurde car $f(U) ≠ f(V)$. On a donc prouvé $¬P$. Finalement, dans tous les cas, on a $P ∨ ¬P$. ∎

Maintenant, voyons comment cette preuve peut se traduire en Coq. L'ensemble $\{⊥, ⊤\}$ va bien sûr devenir le type inductif bool. Comme d'habitude, on va encoder les sous-ensembles $U$ et $V$ par des prédicats, donc U : bool -> Prop := fun b => b = false \/ P et V : bool -> Prop := fun b => b = true \/ P. De même, on va traduire $\{U, V\}$ comme sous-ensemble de $𝒫(\{⊥, ⊤\})$ par UV : (bool -> Prop) -> Prop := fun S => S = U \/ S = W. Ici, toutefois, on peut déjà apercevoir une pomme de discorde se profiler car on est en train d'écrire des égalités entre fonctions…

Chacun de $U$ et $V$ étant habité, on peut prouver forall S, UV S -> exists b, S b. Pour le mettre sous la forme qu'attend le déplacement de troncature, on peut transformer ceci en forall T : {S | UV S}, inhabited {b | let (S, _) := T in S b}. Mais une deuxième pomme de discorde vient de se glisser : on va devoir convertir U en un terme U' : {S | UV S} en lui adjoignant une preuve de UV U, et de même pour V, mais l'égalité U' = V' contient alors une égalité de preuves…

Le déplacement de troncature nous fournit f : forall T : {S | UV S}, {b | let (S, _) := T in S b}. On peut faire des disjonctions de cas sur les booléens contenus dans f U' et f V', et comme précédemment, se ramener au cas où ils valent respectivement true et false. Désormais, le nerf de la guerre est la preuve de U' = V'. Une fois ceci fait, on peut conclure à une contradiction avec le fait que les booléens extraits de f U' et f V' sont différents.

En se rappelant que U' est U auquel est adjointe une preuve de UV U, et de même pour V, il suffit de prouver U = V, mais à condition d'utiliser ensuite l'axiome d'indiscernabilité des preuves pour l'égalité entre les deux preuves. (On ne peut pas espérer qu'elles soient définitionnellement les mêmes : pour prouver UV U := U = U \/ U = V, il faut prendre la branche de gauche, alors que pour prouver UV V := V = U \/ V = V, on prend la branche de droite.)

Pour prouver l'égalité entre U := fun b => b = false \/ P et V := fun b => b = true \/ P, on n'a guère le choix : il faut accepter d'utiliser l'extensionnalité fonctionnelle. Et ce n'est pas fini : on est maintenant ramenés à b = false \/ P = b = true \/ P, or on a seulement b = false \/ P <-> b = true \/ P : il faut donc faire appel aussi à l'extensionnalité propositionnelle.

Au total, on a eu besoin de trois axiomes : extensionnalité fonctionnelle, extensionnalité propositionnelle, et indiscernabilité des preuves. En se rappelant que l'indiscernabilité des preuves est une conséquence immédiate de l'extensionnalité propositionnelle (car sous l'extensionnalité propositionnelle, toute proposition vraie est égale à True, qui n'a qu'une seule preuve), la preuve utilise finalement l'extensionnalité fonctionnelle et propositionnelle.

Voici une formalisation qui clarifie tous les détails. Notez que j'ai caché un peu de poussière sous le tapis dans mon explication en français : les réécritures à la fin sont légèrement délicates à cause des types dépendants. Par exemple, dans la preuve de E2, on ne peut pas faire simplement rewrite E1. après le unfold U, V. car le terme contient des preuves dont les types dépendent de U et V, et le remplacement de U par V donnerait un terme intypable. De même, on peut prouver E3 : proj1_sig (f U') = proj1_sig (f V') par un simple rewrite E2., où E2 : U' = V', mais on ne pourrait pas prouver f U' = f V' parce que ce n'est pas bien typé.

Cette preuve est une simplification d'une partie du module Logic.Diaconescu.

Axiom truncation_shift :
  forall (X : Type) (Y : X -> Type),
    (forall x, inhabited (Y x)) -> inhabited (forall x, Y x).

Axiom funext : forall (X Y : Type) (f g : X -> Y), (forall x, f x = g x) -> f = g.
Axiom propext : forall P Q : Prop, (P <-> Q) -> (P = Q).

Corollary proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
Proof.
  intros. assert (P = True). { apply propext. tauto. }
  subst P. destruct p1, p2. reflexivity.
Qed.

Theorem LEM : forall P : Prop, P \/ ~P.
Proof.
  intros P.
  set (U := fun b => b = false \/ P).
  set (V := fun b => b = true \/ P).
  set (UV := fun S => S = U \/ S = V).
  assert (H : forall T : {S | UV S}, inhabited {b | let (S, _) := T in S b}). {
    intros [S HS]. destruct HS; subst S.
    - constructor. exists false. unfold U. tauto.
    - constructor. exists true. unfold V. tauto.
  }
  destruct (truncation_shift _ _ H) as [f].
  unshelve eset (U' := _ : {S | UV S}). { exists U. unfold UV. tauto. }
  unshelve eset (V' := _ : {S | UV S}). { exists V. unfold UV. tauto. }
  destruct (f U') as [u Hu] eqn:EU. destruct u.
  1: { compute in Hu. destruct Hu. discriminate. tauto. }
  destruct (f V') as [v Hv] eqn:EV. destruct v.
  2: { compute in Hv. destruct Hv. discriminate. tauto. }
  right. intros HP.
  assert (E1 : U = V). {
    apply funext. intros b. apply propext. unfold U, V. tauto.
  }
  assert (E2 : U' = V'). {
    unfold U', V'.
    enough (forall (p : UV U) (q : UV V), exist _ U p = exist _ V q) by firstorder.
    rewrite E1. intros p q. assert (p = q) by apply proof_irrelevance.
    subst p. reflexivity.
  }
  assert (E3 : proj1_sig (f U') = proj1_sig (f V')). {
    rewrite E2. reflexivity.
  }
  rewrite EU, EV in E3. compute in E3. discriminate.
Qed.

Je termine par une petite comparaison à Type. Si au début de cette preuve on remplace

set (UV := fun S => S = U \/ S = V).

par

set (UV := fun S => {S = U} + {S = V}).

… on se rend compte que le reste passe assez bien, à quelques petites modifications près, notamment le {S | UV S} qui forcément devient {S & UV S}, et au passage, on n'a même plus besoin du déplacement de troncature puisque {S = U} + {S = V} peut être éliminé dans Type sans avoir besoin de passer par inhabits. L'endroit qui coince est l'utilisation de l'axiome d'indiscernabilité des preuves, qui ne fonctionne que dans Prop, et pour cause, les preuves d'existence dans Type sont discernables (on peut extraire leurs témoins). Voici la preuve modifiée, avec un admit à cet endroit :

Axiom funext : forall (X Y : Type) (f g : X -> Y), (forall x, f x = g x) -> f = g.
Axiom propext : forall P Q : Prop, (P <-> Q) -> (P = Q).

Corollary proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
Proof.
  intros. assert (P = True). { apply propext. tauto. }
  subst P. destruct p1, p2. reflexivity.
Qed.

Theorem LEM : forall P : Prop, P \/ ~P.
Proof.
  intros P.
  set (U := fun b => b = false \/ P).
  set (V := fun b => b = true \/ P).
  set (UV := fun S => {S = U} + {S = V}).
  assert (f : forall T : {S & UV S}, {b & let (S, _) := T in S b}). {
    intros [S HS]. destruct HS; subst S.
    - exists false. unfold U. tauto.
    - exists true. unfold V. tauto.
  }
  unshelve eset (U' := _ : {S & UV S}). { exists U. unfold UV. tauto. }
  unshelve eset (V' := _ : {S & UV S}). { exists V. unfold UV. tauto. }
  destruct (f U') as [u Hu] eqn:EU. destruct u.
  1: { compute in Hu. destruct Hu. discriminate. tauto. }
  destruct (f V') as [v Hv] eqn:EV. destruct v.
  2: { compute in Hv. destruct Hv. discriminate. tauto. }
  right. intros HP.
  assert (E1 : U = V). {
    apply funext. intros b. unfold U, V. apply propext. tauto.
  }
  assert (E2 : U' = V'). {
    unfold U', V'.
    enough (forall (p : UV U) (q : UV V), existT _ U p = existT _ V q) by firstorder.
    rewrite E1. intros p q.
    assert (p = q). {
      Fail apply proof_irrelevance.
      admit.
    }
    subst p. reflexivity.
  }
  assert (E3 : projT1 (f U') = projT1 (f V')). {
    rewrite E2. reflexivity.
  }
  rewrite EU, EV in E3. compute in E3. discriminate.
Admitted.

Voici comment je résumerais l'intuition qui est derrière les détails techniques de ces preuves. Dans un monde de topos, on peut créer deux objets qui si une proposition est vraie vont devenir égaux par extensionnalité, et en demandant à l'axiome du choix de définir une fonction sur l'ensemble de ces deux objets, on peut le forcer à décider s'ils sont égaux. En théorie des types, la fonction ne prend pas seulement l'un ou l'autre des deux objets, mais aussi la preuve qu'il est égal à l'un ou l'autre. Si ces preuves vivent dans Type, les objets augmentés des preuves deviennent différents. En revanche, si les preuves vivent dans Prop, l'indiscernabilité des preuves les rend égales, et on retrouve le même phénomène.

J'avoue que je ne sais pas très bien quoi en penser, sinon que les axiomes d'extensionnalité ne sont pas aussi anodins qu'ils peuvent le sembler. Si vous croisez l'extensionnalité propositionnelle dans la rue, vérifiez que vous avez toujours votre portefeuille.

Ajout (24 novembre) : En travaillant légèrement plus, on peut remplacer les fonctions bool -> Prop par des paires Prop*Prop et ainsi se passer de l'extensionnalité fonctionnelle.

Axiom truncation_shift :
  forall (X : Type) (Y : X -> Type),
    (forall x, inhabited (Y x)) -> inhabited (forall x, Y x).

Axiom propext : forall P Q : Prop, (P <-> Q) -> (P = Q).

Corollary proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
Proof.
  intros. assert (P = True). { apply propext. tauto. }
  subst P. destruct p1, p2. reflexivity.
Qed.

Theorem LEM : forall P : Prop, P \/ ~P.
Proof.
  intros P.
  set (UV := fun S => S = (True, P) \/ S = (P, True)).
  set (either := fun (T : {S | UV S}) =>
                   let (AB, _) := T in let (A, B) := AB in {A} + {B}).
  assert (H : forall T, inhabited (either T)). {
    intros [S HS]. destruct HS; subst S; firstorder.
  }
  destruct (truncation_shift _ _ H) as [f].
  destruct (f (exist UV (True, P) (or_introl eq_refl))) as [i | HP] eqn:EU.
  2: { left. apply HP. }
  destruct (f (exist UV (P, True) (or_intror eq_refl))) as [HP | i'] eqn:EV.
  1: { left. apply HP. }
  right. intros HP.
  assert (E : P = True). { apply propext. tauto. }
  set (which := fun (A B : Prop) (H : UV (A, B)) =>
                  match (f (exist UV (A, B) H))
                  with left _ => false | right _ => true end).
  assert (A : forall p1 p2, which True P p1 = which P True p2).
  { rewrite E. intros p1 p2. f_equal. apply proof_irrelevance. }
  specialize (A (or_introl eq_refl) (or_intror eq_refl)).
  unfold which in A. rewrite EU, EV in A. discriminate.
Qed.

Commentaires