Tous les commentaires

Commentaire de Jean Abou Samra sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (13 décembre 2024 à 17:31)

J'ai posé une question précise avec plein de détails sur https://proofassistants.stackexchange.com/questions/4532/does-cic%cf%89-prove-conzf.

Commentaire de Jean Abou Samra sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (7 décembre 2024 à 14:35)

En vrac :

L'entrée de la Stanford Encyclopedia of Philosophy sur CZF et IZF mentionne aussi l'interprétation des ensembles en MLTT par un W-type, qui revient au même que ce type inductif en Coq (interprétation proposée par Aczel, cité par Werner). Ça me conforte dans l'idée que c'est vraiment cette possibilité de créer des W-types ou types inductifs qui est essentielle.

Je suis tombé aussi sur ce document. Pour le remplacement (page 15), il utilise manifestement une traduction qui transforme les $∃$ de la théorie des ensembles en $Σ$ du côté théorie des types. À méditer…

Commentaire de Jean Abou Samra sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (5 décembre 2024 à 02:25)

En fait, le HoTT Book fait précisément ce que j'ai fait ci-dessus, cf. théorème 10.5.8 (dans sa version courante à ce jour, first-edition-15-ge428abf).

Commentaire de Jean Abou Samra sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (4 décembre 2024 à 20:36)

Page 12 du papier, je vois :

$$\begin{align*} &\text{Inductive} \ \textsf{Set} : \textsf{Type}_{i+1} \coloneqq \\ &\textsf{sup} : \prod A : \textsf{Type}_i. (A → \textsf{Set}) → \textsf{Set}. \end{align*}$$

où il explique que $\textsf{sup} \ A \ f$ est censé se comprendre comme l'ensemble $\{f(a), a : A\}$. Ensuite, il interprète les quantificateurs de ZFC par des forall X : Set et exists X : Set. (C'est très « confusant » parce que Set est normalement autre chose en Coq, mais ce ne l'était peut-être pas à l'époque, je ne sais pas.)

On retrouve son code sur https://github.com/rocq-archive/zfc. C'est du Coq très vieux, mais ça m'a aidé à comprendre ce qu'il fait. Je me suis amusé à en refaire une partie de manière un peu différente :

Inductive V : Type :=
| sup : forall (X : Type), (X -> V) -> V.

(*
NB : Les univers sont comme ceci :

Inductive V@{u} : Type@{u+1} :=
    sup : forall X : Type@{u}, (X -> V@{u}) -> V@{u}.
*)

Fixpoint Veq (A B : V) {struct A} : Prop :=
  let (X, f) := A in
  let (Y, g) := B in
  (forall x : X, exists y : Y, Veq (f x) (g y))
  /\ (forall y : Y, exists x : X, Veq (f x) (g y)).

Definition Vin (a A : V) : Prop :=
  let (X, f) := A in exists x : X, Veq (f x) a.


Require Import Classes.RelationClasses.

Instance Veq_refl : Reflexive Veq.
Proof.
  intros A. induction A as [X f IH]. split.
  - intros x. exists x. apply IH.
  - intros x. exists x. apply IH.
Qed.

Instance Veq_symm : Symmetric Veq.
Proof.
  refine (fix IH A B := _).
  destruct A as [X f], B as [Y g]. intros [H1 H2]. split.
  - intros y. destruct (H2 y) as [x Hx]. exists x. apply IH. apply Hx.
  - intros x. destruct (H1 x) as [y Hy]. exists y. apply IH. apply Hy.
Qed.

Instance Veq_trans : Transitive Veq.
Proof.
  refine (fix IH A B C := _).
  destruct A as [X f], B as [Y g], C as [Z h].
  intros [H_AB H_BA] [H_BC H_CB]. split.
  - intros x. destruct (H_AB x) as [y Hy]. destruct (H_BC y) as [z Hz].
    exists z. apply (IH (f x) (g y) (h z)). apply Hy. apply Hz.
  - intros z. destruct (H_CB z) as [y Hy]. destruct (H_BA y) as [x Hx].
    exists x. apply (IH (f x) (g y) (h z)). apply Hx. apply Hy.
Qed.

Instance Veq_equiv : Equivalence Veq.
Proof.
  split; [apply Veq_refl | apply Veq_symm | apply Veq_trans].
Qed.

Lemma Vin_respects_Veq_right : forall A B : V, Veq A B -> forall c : V, Vin c A -> Vin c B.
Proof.
  intros [X f] [Y g] [H_XY H_YX] c [x Hx].
  destruct (H_XY x) as [y Hy].
  exists y. symmetry. transitivity (f x). symmetry. apply Hx. apply Hy.
Qed.

Lemma Vin_respects_Veq_left : forall a b : V, Veq a b -> forall C : V, Vin a C -> Vin b C.
Proof.
  intros a b E [Z h] [z Hz].
  exists z. transitivity a. apply Hz. apply E.
Qed.

Theorem extensionality : forall A B : V, Veq A B <-> (forall c : V, Vin c A <-> Vin c B).
Proof.
  intros [X f] [Y g]. simpl. split.
  - intros [H_XY H_YX] c. split.
    + intros [x Hx]. destruct (H_XY x) as [y Hy].
      exists y. transitivity (f x). symmetry. apply Hy. apply Hx.
    + intros [y Hy]. destruct (H_YX y) as [x Hx].
      exists x. transitivity (g y). apply Hx. apply Hy.
  - intros H. split.
    + intros x.
      enough (exists y, Veq (g y) (f x)) as [y Hy]. { exists y. symmetry. apply Hy. }
      apply H. exists x. reflexivity.
    + intros y. apply H. exists y. reflexivity.
Qed.

Theorem replacement
  (A : V) (phi : V -> V)
  (phi_respectful : forall x x', Veq x x' -> Veq (phi x) (phi x')) :
  exists B, forall y, Vin y B <-> exists x, Vin x A /\ Veq (phi x) y.
Proof.
  Fail exists (sup V phi).
  destruct A as [X f].
  exists (sup X (fun x => phi (f x))).
  simpl. intros y. split.
  - intros [x Hx]. exists (f x). split.
    + exists x. reflexivity.
    + apply Hx.
  - intros [s [[x Hx] Hs]]. exists x.
    transitivity (phi s).
    + apply phi_respectful. apply Hx.
    + apply Hs.
Qed.

Je définis le type des ensembles V comme lui, l'égalité Veq entre ensembles est l'égalité extensionnelle, Vin modélise l'appartenance, et je prouve que l'égalité est une relation d'équivalence et que l'appartenance lui est compatible (toutes ces preuves sont triviales).

La forme du schéma de remplacement que je prouve est :

Theorem replacement
  (A : V) (phi : V -> V)
  (phi_respectful : forall x x', Veq x x' -> Veq (phi x) (phi x')) :
  exists B, forall y, Vin y B <-> exists x, Vin x A /\ Veq (phi x) y.

Évidemment, comme c'est un schéma d'axiome, on ne peut pas l'encoder parfaitement en un seul théorème Coq, alors j'ai pris en hypothèse une fonction phi : V -> V : ça ne correspond à rien dans ZFC parce que l'univers $V$ est une classe propre, mais je pense que moralement, c'est bien ce qu'on cherche à modéliser. Si $φ$ est une formule ensembliste telle que $∀ x, ∃! y, φ(x, y)$ soit prouvable dans IZF (ou CZF ? je n'ai pas le temps de regarder les différences tout de suite), alors forall x : V, exists! y : V, phi_rel x y va être prouvable en Coq pour une traduction raisonnable phi_rel : V -> V -> Prop de $φ$ (parce que la traduction de chaque axiome est prouvable, je l'ai fait pour l'extensionnalité, je n'ai pas le courage de faire le reste), et il faut alors une variante du choix pour passer à phi : V -> V. De plus, pour phi obtenue de cette manière, l'hypothèse phi_respectful va être prouvable grâce aux compatibilités que j'ai montrées. Tu noteras que le choix n'est nécessaire que pour passer de phi_rel à phi, et d'ailleurs il semblerait qu'on puisse en fait se contenter d'une variante du choix unique.

Maintenant, dans la preuve de replacement, j'ai laissé au début Fail exists (sup V phi). pour montrer, comme on peut s'y attendre, définir « $B \coloneqq \{φ(x), x ∈ V\}$ » ne marche pas pour cause d'univers (car V vit un univers au-dessus que l'argument de son constructeur). Sauf que comme l'ensemble A est représenté par un type « support » X et une fonction f : X -> V, on peut réutiliser ce support X en composant juste f par phi, et le reste est trivial.

Ma conclusion, c'est que je ne trouve pas que TTDA cache insidieusement une forme de remplacement, et j'ai plutôt l'impression que c'est la possibilité de définir ce type inductif V qui est puissante. Loïc Pujet dit que CCω se trouve strictement entre Z et ZF, mais ici on parle de CICω, et j'en déduis que CICω doit être nettement plus fort que CCω, whatever that means.

Commentaire de Gro-Tsen sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (4 décembre 2024 à 15:43)

Ce n'est pas non plus clair pour moi pourquoi l'axiome TTDA implique Remplacement/Collection, mais Werner dit que c'est le cas (“the encoding of the following collection scheme can be proved in CIC, assuming TTDA” : comme CIC en soi n'est pas spécialement fort, c'est vraisemblablement que TTDA cache une forme de Remplacement de façon insidieuse sous le typage). Comme la preuve est renvoyée à un fichier Coq sans aucune explication supplémentaire, je n'ai pas vraiment envie de comprendre plus. Je suppose que c'est un peu comme Ensembles de Bourbaki, dont il y a une sorte de légende urbaine selon laquelle il omet l'axiome de Remplacement et est donc équivalent à la théorie des ensembles de Zermelo, alors qu'en fait le Replacement est insidieusement caché dans un des autres axiomes (Union, probablement).

Pour la force du Remplacement, notons quand même qu'IZF interprète ZF(C), donc il a la même force : si on veut bien considérer qu'IZF est constructif, la limitation n'est ainsi pas vraiment liée au problème d'être constructif ou pas mais plutôt d'être « ensembliste » ou pas. Mais c'est peut-être quand même aussi lié à la question de savoir si on peut définir correctement des ordinaux constructivement, et à ce que l'itération des ordinaux permet de faire (cf. cet article intéressant à ce sujet). Je n'ai pas les idées claires.

Commentaire de Jean Abou Samra sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (4 décembre 2024 à 01:51)

Tu as raison, je vais corriger ça.

Dans “Sets in Types, Types in Sets”, Werner obtient bien des choses comparables à ZFC, mais c'est en ajoutant des axiomes qui sont une version à peine déguisée de l'axiome de Remplacement.

Je suis beaucoup moins fort que je le voudrais en théorie des ensembles, et je n'ai que très rapidement survolé le papier, donc je dis possiblement des bêtises, mais où est-ce que tu vois des axiomes qui ressemblent au remplacement ? Je ne vois que $\text{TTDA}_i$ et $\text{TTCA}_i$ page 10, qui sont des variantes de l'axiome du choix, non ? (Il sont trivialement impliqués par l'axiome du choix global tel que défini au billet précédent.)

À noter que si la force logique de Coq avec tiers exclu ou carrément avec un avatar du choix est une question intéressante en soi, en l'occurrence ça ne va rien changer parce que je parlais uniquement de complexité de la normalisation, donc on se fiche des axiomes qui peuvent être ajoutés vu qu'ils ne viennent pas avec des règles de réduction (ils cassent la canonicité).

Et au passage, j'avoue que je partage ta perplexité sur l'axiome du remplacement. Pour être honnête, autant je crois fermement à l'axiome du choix, dans une vision platonicienne assumée de la hiérarchie cumulative (même si les maths sans l'axiome du choix m'intéressent, pour des raisons analogues à celles qui rendent les maths constructives intéressantes à mes yeux bien que je croie au tiers exclu), autant je ne suis pas parfaitement sûr à 100% de croire platoniquement à l'axiome du remplacement. Quant à la logique qu'implémente Coq, je n'ai pas les idées très claires là-dessus.

Commentaire de Gro-Tsen sur Les subtilités de Coq, épisode 3 : systèmes de typage purs (3 décembre 2024 à 19:22)

« La force de Coq est comparable à celle de ZFC » → Alors, non, je ne crois vraiment pas. J'avais essayé de résumer les choses dans un vieux billet de mon blog, auquel je viens d'ailleurs d'ajouter un lien vers une réponse de Loïc Pujet sur le StackExchange des assistants de preuves qui répond à des questions analogues, et j'ajoute le disclaimer que tout ça est complètement confus et je m'y perds beaucoup (dans les résultats avec ou sans tiers exclu ou autre gimmick du même genre, sachant que le tiers exclu augmente beaucoup la force de certains systèmes de preuves mais pas de certains autres) et qu'en plus j'ai oublié des choses que j'avais comprises il y a 10 ans, mais de ce que je comprends, la force logique de Coq sans tiers exclu est plutôt comparable à diverses variations de la théorie des ensembles de Zermelo, et pas du tout de ZFC. Dans “Sets in Types, Types in Sets”, Werner obtient bien des choses comparables à ZFC, mais c'est en ajoutant des axiomes qui sont une version à peine déguisée de l'axiome de Remplacement.

Il faut bien se dire que l'axiome de Remplacement, c'est une sorte d'axiome de grand cardinal (qui, je ne sais pas pourquoi, est devenue standard) : en gros elle dit « la classe des ordinaux est un cardinal inaccessible », et c'est vraiment fort, en fait.

Je ne crois pas qu'on sache faire quoi que ce soit qui ressemble à ZFC en force logique (sans parler des différentes saveurs de grands cardinaux qu'on sait y ajouter) et qui ne soit pas essentiellement une transposition de ZFC dans des termes à peine déguisés. C'est un peu mystérieux : il n'y a que sur des fondements ensemblistes qu'on arrive à justifier des résultats arithmétiquement très forts (et qu'on pense vrais, évidemment). En tout cas, Coq est loin du compte (sauf s'il y a eu des développements que j'ignore).

Commentaire de Informatheux sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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.

Commentaire de Informatheux sur Pourquoi est-ce que personne ne parle du chat control ? (12 novembre 2024 à 14:49)

En réalité, je pense que personne ne parle du ChatControl en France parce que tout le monde s'en fiche, que ce soit la société civile ou la classe politique. Le "je n'ai rien à me reprocher" a de beaux jours devant lui. Il ne reste guère plus que quelques chercheurs, développeurs et autres professionnels de l'informatique, ainsi que les irréductible de la Quadrature du Net pour se plaindre à haute voix des dérives sécuritaires de la technopolice et de la société de la surveillance.

Commentaire de Informatheux sur Rions trois fois par sacs de deux : quelques extraits d'articles scientifiques (12 novembre 2024 à 14:45)

Je pense qu'il faut mentionner quelques pépites de Pierre-Marie Pédrot, comme :

Un thésard demanda à Hugo Herbelin : « Coq est-il cohérent ? »
Anomaly: Uncaught exception Mu.

Une Dialectica Matérialiste

Sheaves were first introduced in French as faisceaux. Owing to this Romance etymology, and noting the lack of a corresponding formal Germanic counterpart, we are forced to conclude that the adjectivization of sheaf is fascist, fitting their authoritarian meta-theory.

Russian Constructivism in a Prefascist Theory

ou les noms de ses articles de manière générale, comme celui que je viens de citer ou An Effectful Way to Eliminate Addiction to Dependence

Commentaire de Jean Abou Samra sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Gro-Tsen sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Jean Abou Samra sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Gro-Tsen sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Gro-Tsen sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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.

1. 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 Jean Abou Samra sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Jean Abou Samra sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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.

Commentaire de DmxLarchey sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Jean Abou Samra sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Gro-Tsen sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Gro-Tsen sur Les subtilités de Coq, épisode 1 : élimination des sous-singletons (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 Pileum sur Lettre au ministère de l'intérieur (21 octobre 2024 à 03:14)

Non, je ne me rappelle pas de tels détails.

Commentaire de Jean Abou Samra sur Lettre au ministère de l'intérieur (19 octobre 2024 à 16:25)

Bonjour et merci pour votre commentaire. Je n'ai pas de réponse pour l'instant. C'est intéressant que cette annonce ait été faite ; ont-ils aussi dit pourquoi ils ne l'avaient pas encore fait, quels étaient les obstacles ?

Commentaire de Pileum sur Lettre au ministère de l'intérieur (19 octobre 2024 à 00:17)

Merci d'avoir pris le temps d'envoyer ce courrier, avez-vous reçu leur réponse ?

Je souhaite ajouter que, lors d'un webinaire organisé par France Identite le mardi 20 février 2024 (https://www.linkedin.com/posts/programme-interminist-riel-france-identit-num-rique_webinaire-de-pr%C3%A9sentation-de-lapplication-activity-7164259958732046336-y_WF), la question de l'ouverture des codes sources a été posée lors de la séance de questions/réponses. Florent TOURNOIS, directeur de projet France Identité, a répondu que cela était prévu prochainement.

Commentaire de Gro-Tsen sur Pourquoi est-ce que personne ne parle du chat control ? (9 octobre 2024 à 23:42)

Pour être plus clair, Meredith Whittaker a dit qu'elle n'obéirait pas à la loi, pas qu'elle quitterait volontairement le marché européen. C'est important, parce que ça pose la question de se qui se passerait après : il est difficile d'interdire un logiciel libre, et pas très commode non plus de filtrer ses serveurs (le plus évident est de juste dire à Google et Apple de retirer l'app de leurs app stores). Et ça étale bien l'hypocrisie de toute la manip : c'est que c'est tellement trivial à contourner que c'est un règlement qui va être appliqué de façon complètement sélective aux moyens de communication qu'on a envie de contrôler, et donc juste créateur d'insécurité juridique.

Commentaire de zonetuto sur Pourquoi est-ce que personne ne parle du chat control ? (9 octobre 2024 à 09:27)

Article très intéressant et détaillé merci beaucoup, je ne connaissais pas l'existence du Chat Control ...

Commentaire de Jean Abou Samra sur Email et désespoir (7 octobre 2024 à 11:34)

Intéressant, il faudra que je me renseigne mieux sur XMPP. Et votre article futur sur Matrix m'intéresse, n'hésitez pas à poster le lien ici quand vous l'aurez écrit !

Commentaire de Djan Gicquel sur Email et désespoir (7 octobre 2024 à 07:54)

Ce n'est pas un problème pour l'usage des réseaux sociaux, c'en est un pour remplacer l'email car j'ai besoin de conserver les emails que je reçois sur le long terme, je serais embêté si certains disparaissaient parce que l'hébergeur de l'expéditeur n'est plus disponible.

Avec XMPP les messages sont conservés sur les appareils. La plupart des serveurs supprimment les messages après un certain délai. Matrix présente de grandes failles en terme de sécurité, j'ai l'intention d'écrire un article sur le sujet.

Commentaire de Jean Abou Samra sur Email et désespoir (2 octobre 2024 à 11:53)

Merci pour votre commentaire, et désolé de répondre tard. Il est concevable que des extensions des protocoles puissent transformer des réseaux sociaux décentralisés existants en outils de communication personnelle, mais en l'état je n'en vois aucun qui pourrait remplir ce rôle. Par exemple, sur Mastodon (celui que je connais le mieux), les messages qu'on vous envoie restent stockés sur le serveur de l'expéditeur. Ce n'est pas un problème pour l'usage des réseaux sociaux, c'en est un pour remplacer l'email car j'ai besoin de conserver les emails que je reçois sur le long terme, je serais embêté si certains disparaissaient parce que l'hébergeur de l'expéditeur n'est plus disponible.

Quant à XMPP et Matrix, je n'y connais pas grand-chose mais j'ai cru comprendre qu'ils étaient vraiment tournés vers la messagerie instantanée.

Commentaire de Djan Gicquel sur Email et désespoir (23 septembre 2024 à 09:11)

Bonjour Jean, J'ai lu avec beaucoup d'attention votre article sur les emails et je vous rejoins sur tous les points cités.

Avec tous les réseaux sociaux libres et décentralisé qui existent (beaucoup trop à mon goût) il n'y aurait pas déjà un, voir plusieurs, remplaçants acceptables ?

Commentaire de Jean Abou Samra sur Email et désespoir (11 juin 2024 à 23:44)

Il me semble (je n'en suis pas certain) que la clé privée de France Identité est uniquement stockée dans la puce de la carte d'identité. Enfin, il faudrait que je me renseigne.

Commentaire de Informatheux sur Email et désespoir (11 juin 2024 à 23:41)

Aussi, il faut que ce soit facile à mettre à jour, et inviolable, dans la même veine que : si mon mot de passe fuite, je peux le changer, si mon emprunte digitale fuite, je suis foutu.

Commentaire de Jean Abou Samra sur Email et désespoir (11 juin 2024 à 23:40)

Ça, c'est pas faux, et j'avoue que je n'y avais pas pensé. Il faudrait sans doute des protections de type RGPD pour que les sites doivent accepter aussi les adresses anonymes. Enfin, il faudrait que je réfléchisse aux conséquences de ce type plus sérieusement.

Commentaire de Informatheux sur Email et désespoir (11 juin 2024 à 23:39)

Je comprends tout à fait, mais je pense que ça ne fournira pas une solution pérenne. Il y aura toujours plein d'arnaques et ce qu'il faut faire c'est éduquer à leur sujet (ne jamais payer de rançons, ne pas faire confiance aux mails douteux, vérifier par un autre canal si possible, etc.) Bien sûr que les mails importants soient signés serait très pertinent mais l'authentification des personnes privées, j'en doute.

Ça me fait penser à l'adolescent de y a un ou deux ans qui avait été embobiné par un brouteur qui le faisait chanter, il a demandé de l'argent à ses parents pour le payer (sans leur dire pourquoi évidemment ; plusieurs centaines d'euros), ils ont refusé et du coup il s'est suicidé parce que le brouteur menaçait de divulguer des photos intimes (je ne sais plus si le brouteur en avait pour de vrai ou faisait juste semblant) 😢

Commentaire de Jean Abou Samra sur Email et désespoir (11 juin 2024 à 23:32)

Alors petite anecdote personnelle : le jour où j'en ai reçu un quand j'étais plus jeune (peut-être en seconde), j'étais complètement paniqué. N'ayant jamais regardé de porno, je voyais bien que c'était forcément pipo, mais le fait qu'il semble provenir de ma propre adresse m'affolait vraiment (évidemment, je n'avais pas la compréhension technique que j'ai aujourd'hui).

Commentaire de Informatheux sur Email et désespoir (11 juin 2024 à 23:31)

Par exemple, un site internet pourrait exiger une preuve d'identité alors qu'il n'en a pas besoin. Ce serait facile si tout le monde avait à sa disposition une preuve d'identité liée à son mail.

Commentaire de Jean Abou Samra sur Email et désespoir (11 juin 2024 à 23:29)

Après, sur l'extension à d'autres domaines, j'ai un peu de mal à imaginer ce que ça donnerait parce que pour moi c'est évident que ça n'a rien à voir par exemple avec les réseaux sociaux, mais je sous-estime peut-être la capacité à séparer les débats.

Commentaire de Informatheux sur Email et désespoir (11 juin 2024 à 23:27)

Moi les spams que je reçois c'est surtout des newsletters auxquelles je ne me suis pas abonné et des mails de prospection commerciale non sollicités.

Par ailleurs, pour les mails du type "j'ai pris le contrôle de ton ordinateur", c'est du bon sens de ne pas payer les pirates, rien à voir avec une éventuelle authentification. Quant aux mails frauduleux soi-disant d'une banque, je suis tout à fait d'accord qu'un mécanisme type PGP serait très utile, mais une banque c'est pas un citoyen lambda.

Commentaire de Jean Abou Samra sur Email et désespoir (11 juin 2024 à 23:26)

Sur ce dernier point, on ne doit pas recevoir les mêmes spams 🙂 Sur mon adresse perso, j'en ai très peu (un peu miraculeusement car elle circule de manière publique à certains endroits, notamment des commits Git), mais je suis admin de plusieurs mailing lists, où j'en vois passer une vingtaine par jour, et il y a plein d'usurpations d'identité dans le lot, même si elles sont loin d'être majoritaires :

— Les mails qui prétendent que ton compte mail va être bloqué si tu ne fais pas une « authentification de sécurité », ou que tu as des messages non délivrés en attente et qu'il faut te connecter à ton webmail pour les voir, qui cherchent obtenir le mot de passe de ta boîte mail. (Ok, c'est l'identité d'une organisation qui est usurpée, pas d'une personne, j'aurais pu en parler mais je commençais à fatiguer.)

— Les « information confidentielle reçue de la Banque Postale / Crédit mutuel / etc. , connectez-vous pour lire le message. » pour te dérober tes identifiants bancaires.

— Les emails qui semblent venir de l'adresse même du destinataire : « J'ai pris le contrôle de ton ordinateur, et pour preuve, je t'envoie ce message depuis ta propre adresse. J'ai pris un enregistrement de ta webcam où on te voit regardant du porno, tu as le choix de me verser tant sur ce portefeuille Bitcoin ou que j'envoie cette vidéo à tous tes contacts. »

— Et une fois, il y a eu une vague de spams envoyés directement à des membres avec comme From: des adresses de têtes connues sur ces listes (dont ma propre adresse). Avec des liens « document partagé avec vous », mais je n'ai pas cliqué pour savoir quel type d'arnaque c'était.

Commentaire de Informatheux sur Email et désespoir (11 juin 2024 à 19:36)

Plusieurs remarques : Pour le format des mails, je pense que markdown serait pas mal ;

Pour les threads, il faudrait surtout une structure de DAG ;

Pour l'authentification je suis contre :

1. Si une procédure d'authentification existe, il sera quasiment impossible d'empêcher son extension à tous les domaines.
2. C'est probablement impossible à mettre en œuvre a un niveau international.
3. Il est très rare d'avoir des mails qui se font passer pour quelqu'un d'autre. Quand ma grand-mère s'est fait arnaquer, c'est sa belle-sœur qui lui demandait soi-disant de l'argent. L'adresse mail était la même mais avec un i doublé, ce qui se voit peu, mais le champ From: était correct. Et ce qui aurait dû lui mettre la puce à l'oreille c'est qu'elle lui demande par mail 1000€ alors qu'elles se voient régulièrement et qu'elle aurait vérifier par téléphone, pas le i en trop.