La risposta breve alla tua prima domanda è: in generale, non è possibile, ma nel tuo caso particolare, sì.
Nella teoria di Coq, le proposizioni (vale a dire, Prop s) e le loro dimostrazioni hanno uno stato molto speciale. In particolare, in generale non è possibile scrivere un operatore di scelta che estrae il testimone di una prova di esistenza. Questo viene fatto per rendere la teoria compatibile con certi assiomi e principi, come la prova dell'irrilevanza, che dice che tutte le prove di una determinata proposizione sono uguali tra loro. Se vuoi essere in grado di farlo, devi aggiungere questo operatore di scelta come un assioma aggiuntivo alla tua teoria, come nel caso standard library.
Tuttavia, in alcuni casi particolari, è è possibile estrarre un testimone da una prova di esistenza astratta senza ricorrere a ulteriori assiomi. In particolare, è possibile farlo per tipi numerabili (come Z) quando la proprietà in questione è decidibile. Ad esempio, è possibile utilizzare l'interfaccia choiceType nella libreria Ssreflect per ottenere esattamente ciò che si desidera (cercare la funzione xchoose).
Detto questo, di solito consiglierei contro di fare cose con questo stile, perché porta a una complessità non necessaria. È probabilmente più semplice definire Good direttamente, senza ricorrere alla prova dell'esistenza, e quindi provare separatamente che Good ha la proprietà ricercata.
Definition Good : Z := (* ... *)
Definition IsGood (z : Z) : Prop := (* ... *)
Lemma GoodIsGood : IsGood Good.
Proof. (* ... *) Qed.
Lemma GoodUnique : forall z : Z, IsGood z -> z = Good.
Se si vuole assolutamente definire Good con una prova di esistenza, è anche possibile modificare la prova della Lemma_GoodExistsUnique utilizzare un connettivo Type invece di Prop, in quanto permette di estrarre il testimone direttamente utilizzando la funzione proj1_sig :
Lemma Lemma_GoodExistsUnique : {z : Z | Good z /\ forall z', Good z' -> z' = z}.
Proof. (* ... *) Qed.
Per quanto riguarda la seconda domanda, sì, è un po 'correlata al primo punto. Ancora una volta, ti raccomanderei di annotare una funzione y_from_x con tipo Z -> Z che calcolerà dato x e poi dimostrerà separatamente che questa funzione mette in relazione ingressi e uscite in un modo particolare. Quindi, è possibile affermare che gli s sono diversi per x s provando che y_from_x è iniettivo.
D'altra parte, non sono sicuro di come il tuo ultimo esempio si riferisce a questa seconda domanda. Se ho ben capito che cosa si vuole fare in modo corretto, è possibile scrivere qualcosa di simile a
Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) :=
exists zs : list Z,
Z.of_nat (length zs) = N
/\ NoDup zs
/\ Forall IsGood zs.
Qui, Z.of_nat : nat -> Z è l'iniezione canonica da naturali a numeri interi, NoDup è un predicato affermando che una lista non contiene elementi ripetuti, e Forall è un predicato di ordine superiore che asserisce che un dato predicato (in questo caso, IsGood) contiene tutti gli elementi di un elenco.
Come nota finale, consiglierei di non usare Z per cose che possono riguardare solo numeri naturali. Nel tuo esempio, utilizzi un numero intero per parlare della cardinalità di un set e questo numero è sempre un numero naturale.