[COQ] Les types ex et sig

[mathys]

Bonjour,

J'essaye d'apprendre COQ. Voici mon problème.
Disons que l'on a A et B de types Set et P de type A -> B -> Prop.
J'ai aussi comme hypothèse que P est en fait une fonction, c'est-à-dire que l'on a

Code :

1
2
Hypothesis Ax1 : forall x:A, exists y:B, (P x y).
Hypothesis Ax2 : forall x:A, forall y1:B, forall y2:B, (P x y1) -> (P x y2) -> y1=y2.

J'aimerais donc introduire f de type A->B tel que l'on ait (P x (f x)) pour tout x:A.

A partir d'un f_aux de type A -> {y:B | (P x y)}, j'arrive à déduire mon f. Mon problème est que je n'arrive pas à définir f_aux. J'ai pensé à écrire quelque chose du genre:

Code :

1
2
Definition f_aux (x:A) : {y:B | (P x y)} := 
match x with x => (exist ??? ).

Dans les ???, j'aurais besoin de mettre quelqu'un de type B. J'ai (Ax1 x) de type exists y:B, (P x y). Je ne peux pas utiliser ex_ind, car ça renvoie un type Prop, et B est de type Set. Comment faire?

Merci à tous ceux qui m'aideront, je suis bloqué.

[gorgonite]

j'ai l'impression que tu souhaites en fait déclarer que

Code :

1
2
exists f : A -> B, forall x:A, forall y:B, (y = (f x)) -> (P x y)

hors ceci est une déclaration d'existence non constructiviste, et n'est normalement pas autorisé par les logiques intuitionnistes (justement ce point et le tiers exclus ont été supprimés par rapport aux logiques classiques)

[mathys]

Merci Gorgonite pour ta réponse. Peut-être as-tu raison. En effet, pour démontrer

exists f : A -> B, forall x:A, forall y:B, (y = (f x)) -> (P x y)

à partir de (Ax1), on a besoin de l'axiome du choix.
Mais si, en plus, on a (Ax2), on n'a plus besoin de l'axiome du choix.
Quelles conséquences cela a en COQ? Peut-être cela veut-il dire que l'on ne peut pas faire ce que je voulais faire en utilisant seulement (Ax1) et il est vrai que mes tentatives jusqu'à présent ne cherchaient pas à utiliser (Ax2). Par contre, avec (Ax2), la définition de f est parfaitement constructiviste, donc je trouverais bizarre que l'on n'y arrive pas en COQ.
Mais peut-être faut-il s'y prendre différemment...

[gasche]

Disclaimer : je ne connais qu'assez mal Coq, et je manque beaucoup de pratique. À prendre avec des pincettes, donc.

Il me semble qu'en Coq, ce qui vit dans Set est intrinsèquement calculable et ce qui vit dans Prop est intrinsèquement non-calculatoire (effacé à l'extraction, etc.). Tu peux donc passer du monde Set au monde Prop (par exemple de "bool" à Prop; il suffit d'oublier le contenu calculatoire), mais pas l'inverse.

Ici tu essaies de convertir un "ex" (Prop) vers une valeur dans Set (la fonction f), et ce n'est pas possible. Ce que tu devrais faire, c'est partir de Set dès le départ, en te donnant une forme calculable de ton premier axiome :

Code :

forall x : A, {y:B | P x y}

Plus tu restes du côté calculable, plus tu pourras faire de chose (par exemple résoudre ton problème), et tu pourras toujours oublier cette calculabilité pour te plonger dans Prop, où tout est possible, plus tard si tu en as envie.

Avec cette définition, j'arrive à prouver que "forall x, P x (f x)", en utilisant uniquement Ax1, et je peux ensuite prouver la réciproque, "forall y, P x y -> y = f x" en utilisant Ax2 et le premier sens (et chaque preuve fait 3 lignes).

Edit : ce message d'alex_pi explique bien les raisons qui rendent l'extraction d'un exist indésirable. À lire.

[mathys]

Merci beaucoup, bluestorm.

Je crois avoir compris que mon erreur fondamentale est que je voulais effectivement avoir une fonction de type ex A P -> A, que ce n'est pas possible et pourquoi c'est bien que ce ne soit pas possible (il peut y avoir plusieurs témoins de l'existentiel et récupérer le témoin donné par la preuve de ex A P, c'est nier l'indiscernabilité des preuves).
J'ai aussi compris pourquoi si au lieu d'avoir comme axiome ex A P, j'ai comme axiome sig A P, on peut faire comme tu dis.
Mais ça ne me satisfait pas. Il me semble naturel que si l'on a : il existe un unique y tel que P y (P de type A -> Prop), que ce soit comme axiome ou que ce soit parce qu'on l'a prouvé, on devrait pouvoir récupérer ce y sans nier l'indiscernabilité des preuves, puisque toutes les preuves de l'existence de ce y donneront obligatoirement le même y comme témoin. Je voulais le faire ainsi : (ex A P) implique (sig A P), qui implique A, mais pour la première implication je cherchais à avoir (ex A P) implique A, ce qui n'est pas possible - si c'était possible, j'aurais même pu me passer du type sig en fait. Ne peut-on pas alors montrer l'existence de la fonction f, mais en utilisant (Ax2) cette fois?

[gasche]

Ce n'est pas parce qu'un élément existe et est unique que tu peux le construire.

Si tu considères que ton "existe" est constructif, tu peux extraire le témoin dans tous les cas; c'est exactement "sig" et c'est ce que tu devrais utiliser si tu supposes l'existence constructive.

Si tu utilises "ex" c'est parce que tu veux la logique plus large et moins calculatoire de Prop, qui peut être utilisée comme une logique classique. Dans ce cadre (logique classique), l'existence et l'unicité ne suffisent pas pour construire la fonction. Par exemple si je prends B = bool et P le prédicat (fun a b => if tiers_exclu probleme_ouvert then b=true else b=false), j'ai trivialement existence et unicité mais ça reste non constructible.


Du reste, ce n'est pas parce que quelque chose est vrai que tu peux nécessairement le faire en Coq exactement comme tu penses. Dans l'espoir de rester simple, Coq impose parfois des restrictions concrètes sur ce qu'on peut faire, qui garantissent la correction mais sont parfois sous-optimales : en faisant des finesses on pourrait avoir un peu mieux (par exemple les critères syntaxiques de terminaison). La règle c'est qu'on "ne peut pas extraire de Prop vers Type", et elle s'applique même si toi tu sais, par des arguments para-coq, que ton autre théorème aurait tendance à dire que, dans ce cas, cette règle est trop restrictive.
Coq est un outil qui permet de faire des mathématiques, mais il faut être prêt à changer un peu la façon dont on fait les choses. La méthode que j'utilise personnellement pour éviter les problèmes, c'est d'être le plus précis possible en matière de constructibilité (je sais construire un témoin => sig, le prédicat est calculable => bool).

[gasche]

La propriété que tu veux utiliser (s'il existe et est unique, je peux le construire) est "l'axiome de choix unique". Il existe dans la bibliothèque standard Coq Logic.ChoiceFacts sous les noms "AC!", "Functional Relation Reification", "principle of definite description". Tu peux en faire un axiome (tout comme on peut commencer un développement Coq en admettant le tiers exclu) si cela correspond aux raisonnements que tu veux faire avec Coq.

Code coq :

1
2
3
4
Definition FunctionalRelReification_on :=
  forall R:A->B->Prop,
    (forall x : A, exists! y : B, R x y) ->
    (exists f : A->B, forall x : A, R x (f x)).

(exists! est un sucre syntaxique pour (ex (unique ..)))

Edit : après une rapide recherche Google, il semblerait qu'on peut prouver en construisant un modèle adéquat que cet "axiome du choix unique" n'est pas prouvable dans le calcul des constructions pur, mais je n'ai pas trouvé de version libre d'accès de l'article l'affirmant (Streicher, 1992).

[mathys]

Merci encore, Bluestorm.

Effectivement, je croyais à tort que l'axiome du choix unique était prouvable. J'ai lu dans la FAQ que c'est un axiome indépendant.
Mon intuition était basée sur le fait que cet axiome me semble parfaitement constructiviste, d'ailleurs dans IZF (ZF intuitionniste), cet axiome est prouvable. Les choses sont plus compliquées que cela...

Admettons donc un moment cet axiome. Il me semble que ça ne me permet pas encore de définir ma fonction. En effet, on se retrouve avec le même problème qu'avant : avant, de l'existence d'un (unique) y tel que (R x y) on ne pouvait pas définir cet y; maintenant de l'existence d'un f tel que forall x:A, (R x (f x)), on ne peut pas définir ce f.
Même en renforçant l'axiome du choix unique en disant que ça définit une unique fonction, je ne pourrai pas écrire

Definition f := A->B.

suivi d'une preuve qui définit f tel que forall x:A, (R x (f x)).

Je crois que je dois me résoudre à accepter que mon désir n'était pas compatible avec la philosophie de Coq. Quelqu'un pour confirmer?