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 :
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.
Partager