Discussion :

[alex_pi]

J'ouvre un autre fil pour ne pas trop pourrir le Quizz fonctionnel

Je voulais apporter quelques précisions relativement au questionnement de DrTopos sur l'existentiel en Coq, le proof-irrelevance (indiscernabilité des preuves en « Français ») et ce genre de choses (désolé pour le retard, je suis en train d'apprendre :-))

Pour vérifier que j'ai bien compris, et si oui pour aider les lecteurs : le principe de "proof-irrelevance" pour un système logique revient à dire que si j'ai une proposition P, et deux preuves p1 et p2 de P, alors, du point de vue du système logique, p1 = p2 même si elles sont "différentes" au sens intuitif de "la façon de montrer". Autre vision de la "proof-irrelevance", il existe deux types de proposition seulement, celles qui sont démontrables et celles qui ne le sont pas (bref, en Coq, ça revient à dire que le type Prop est un type à deux éléments)

Tout d'abord, l'existentiel est défini de la façon suivante :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex P.

qui en gros est une paire de Heyting puisque pour construire un élément de type "ex A P", c'est à dire "il existe x de type A tel que P x", il faut fournir un élément x de type A et une preuve de P x. D'où l'inquiétude : peut-on extraire la première composante de cette paire à l'aide d'un destructeur ? Si oui, on n'aurait évidement pas proof-irrelevance, puisqu'on pourrait discerner deux preuves de "il existe un entier naturel pair" qui prendraient 0 ou 2 comme sus-dit entier.

Or en Coq, on ne peut pas extraire le témoin. La limitation est que l'on ne peux pas extraire d'élément de type Type à partir d'un élément de type Prop. Or dans la définition, le témoin est de type Type et l'existentiel de type Prop, donc on ne peut sortir le témoin !

La raison est double. La première, qui me semble être celle historique, est que lorsque l'on fait de l'extraction de preuve toute donnée de type Prop est ignoré. On considère qu'elles n'ont pas de contenu calculatoire. Donc si on pouvait extraire un élément de type Type d'un élément de type Prop, on jetterai l'élément de type Prop à l'extraction, et l'élément de type Type devrait être créé ex-nihilo (là normalement j'ai perdu tout le monde)

La deuxième raison, qui devrait plus plaire au DrTopos est que les gens qui font Coq ont à coeur de maintenir la compatibilité avec le principe de proof-irrelevance. Ils savent que si l'on ajoute la logique classique et l'opérateur de description à Coq, alors on peut prouver le principe de proof-irrelevance, et que s'il était contradictoire avec le reste du système Coq, cela rendrait impossible l'ajout de ces deux principes qui plaisent quand même bien aux matheux qui font du Coq (il parait que ne pas avoir le droit de faire de disjonction de cas ou de nommer cet unique réel qui monté au carré vaut x leur pose problème. Je ne les comprendrais jamais :-p).

Alors est-il impossible de faire du Martin-Löf, de récupérer le premier élément ? Et bien non ! Le type sig est là pour vous :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
Inductive sig (A:Type) (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

Aucune différence mis à part que c'est de type Type au lieu d'être de type Prop, et que l'on peut donc s'en donner à coeur joie sur l'extraction ! Et lors de l'extraction de programme, l'élément vérifiant l'existentiel sera bien extrait et seul la preuve sera jetée (puisqu'elle a été faite une fois pour toutes)

Pour résumer, Coq n'est pas incompatible avec le principe d'indiscernabilité des preuves (du moins pas de façon connue :-)), et en plus, ça arrange aussi au niveau de l'extraction de programme.

Bref, faites du coq, c'est comme ça

[Steki-kun]

(là normalement j'ai perdu tout le monde)

Non aucun problème, c'est normal Docteur ?

En tout cas je confirme que tout ça est correct, merci pour toutes ces explications elles rendront sûrement plus claire à tout le monde la petite parenthèse où nous avions dérivé avec le Dr Topos dans son Quizz.

Pour faire le lien avec ce qui a été dit sur cet autre fil d'ailleurs, je n'y avais parlé que de la différence entre Prop et Set, mais alex_pi nous introduit le type (la famille de types, en réalité) Type. En fait, c'est bien Type qui correspond aux types Un de la théorie de Per Martin-Löf : en interne il y a une infinité de Types Type0, Type1 etc qui correspondent aux types U0, U1 etc. Du point de vue de l'utilisateur, un type quantifié sur Type reste donc apparement dans Type mais en réalité il passe dans Type(n+1).

Par ailleurs, Set et Prop sont tous deux de type Type dans le CIC, mais à la différence de Prop, Set n'est pas ignoré à l'extraction et est prédicatif. Set peut donc être vu comme un "Type du pauvre", ou un Type(-1) à la base de la famille des Type. Il existe par exemple l'analogue sigS dans Set au sig dans Type montré par alex_pi. (D'ailleurs, je crois que l'existence de Set est historique aussi et remonte à la période où Set était imprédicatif, au contraire de Type0, et qu'aujourd'hui ça ne fait plus beaucoup de sens d'avoir un Set séparé mais si qqun a des détails sur ça je suis preneur).

[alex_pi]

(D'ailleurs, je crois que l'existence de Set est historique aussi et remonte à la période où Set était imprédicatif, au contraire de Type0, et qu'aujourd'hui ça ne fait plus beaucoup de sens d'avoir un Set séparé mais si qqun a des détails sur ça je suis preneur).

D'après le cours de ce matin, il semblerait que le type Set soit effectivement plus là pour des raisons historiques, mais je ne saurais être catégorique.

Je confirme de plus que l'on a une hiérarchie de sortes : Prop C Type1 C Type2... (avec C le symbole d'inclusion) et de plus Prop : Type1 : Type2... (avec : le symbole "est de type")

[DrTopos]

Bonjour.

Je viens juste de m'apercevoir de l'existence de ce fil !

Autre vision de la "proof-irrelevance", il existe deux types de proposition seulement, celles qui sont démontrables et celles qui ne le sont pas (bref, en Coq, ça revient à dire que le type Prop est un type à deux éléments)

Je crois que tu confonds le type Prop (O dans le quizz) et le type p quand p est de type Prop (W(p) dans le quizz). En effet, proof-irrelevance parle d'égalités entre preuves et non pas entre énoncés (propositions). Proof-irrelevance entraine donc que tout type W(....) ne peut pas avoir plus d'un élément. Ce n'est pas la même chose que de dire que O n'a que deux éléments. La preuve est qu'il existe des modèles (celui que je préfère est le topos des préfaisceaux d'ensembles sur l'ordinal 2) qui satisfont proof-irrelevance, mais où O a plus de 2 éléments (il en a 3 dans le cas de mon exemple).

toute donnée de type Prop est ignoré. On considère qu'elles n'ont pas de contenu calculatoire.

Exact, et pour ma part j'analyse ce phénomène comme une conséquence du fait que O n'a pas de destructeur. L'absence de destructeur fait que les données ne sont pas exploitables, même si elles sont manipulables. C'est aussi le cas du type One pour la même raison: pas de destruteur. Ce qui fait que les données de type W(...) sont au contraire exploitables est qu'il y a l'opérateur de description, qui permet de retourner des preuves aux données des types ordinaires. En fait, sans l'opérateur de description, les types O et W(...) seraient des impasses: on pourrait y entrer, mais pas en sortir. Toutefois, sans la description ils auraient quand même une utilité (pour la sureté), mais ne produiraient jamais de code. Avec la description, ils peuvent produire du code.

Du point de vue de l'histoire de Coq, il me semble que l'interdiction de l'extraction Prop -> Type est récente. Il me semble avoir compris que c'est l'introduction de proof-irrelevance qui a forcé cette interdiction qui ne devait pas exister dans les premières versions basées plus ou moins directement sur Martin-Löf (y a-t-il des historiens de Coq dans l'avion ?)

J'ai prévu de parler d'ensembles dans le quizz, mais il me semble que le concept que j'ai en tête n'a pas grand chose à voir avec le type Set de Coq. On verra quand on en sera rendu là.

Une chose aussi à propos du mot ``témoin''. On aura remarqué que l'utilisation qu'en fait alex_pi ci-dessus n'a pas le même sens que le sens que je lui donne dans le quizz. alex_pi utilise le mot ``témoin'' pour désigner le premier composant d'une paire de Heyting. C'est ce que font la plupart des auteurs. J'utilise le mot ``témoin'' pour désigner la sémantique d'une preuve, et ce depuis assez longtemps, en fait avant d'avoir eu connaissance de l'autre utilisation. C'est un peu embêtant, et cela peut en particulier entrainer un contre-sens sur l'expression ``unicité du témoin'' que j'utilise parfois à la place de proof-irrelevance. Si quelqu'un a un autre mot à proposer pour la sémantique d'une preuve il est encore temps de changer, même si je trouve que ``témoin'' convient bien pour désigner ce que représente une preuve puisque cette donnée ``témoigne'' de la vérité de l'énoncé prouvé.