[COQ] Les types ex et sig
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é.