Короткий ответ на ваш первый вопрос: в общем, это невозможно, но в вашем конкретном случае, да.
В теории Кока предложения (т. Е. Prop с) и их доказательства имеют особый статус. В частности, вообще невозможно написать оператор выбора, который извлекает свидетеля доказательства существования. Это делается для того, чтобы теория совместима с некоторыми аксиомами и принципами, такими как доказательство несоответствия, в котором говорится, что все доказательства данного предложения равны друг другу. Если вы хотите это сделать, вам нужно добавить этот оператор выбора в качестве дополнительной аксиомы к вашей теории, как в standard library.
Однако, в некоторых конкретных случаях, это is можно извлечь свидетеля из абстрактного доказательства существования без повторения каких-либо дополнительных аксиом. В частности, это можно сделать для счетных типов (например, Z), когда рассматриваемое свойство разрешимо. Например, вы можете использовать интерфейс choiceType в библиотеке Ssreflect, чтобы получить именно то, что вы хотите (ищите функцию xchoose).
Это, как говорится, я обычно советую против делать вещи в этом стиле, потому что это приводит к ненужной сложности. Вероятно, проще определить непосредственно Good, не прибегая к доказательству существования, а затем доказать, что Good имеет искомое свойство.
Definition Good : Z := (* ... *)
Definition IsGood (z : Z) : Prop := (* ... *)
Lemma GoodIsGood : IsGood Good.
Proof. (* ... *) Qed.
Lemma GoodUnique : forall z : Z, IsGood z -> z = Good.
Если вы абсолютно хотите определить Good с доказательством существования, вы можете также изменить доказательство Lemma_GoodExistsUnique использовать связку в Type вместо Prop, так как она позволяет извлекать свидетель непосредственно с помощью функции proj1_sig :
Lemma Lemma_GoodExistsUnique : {z : Z | Good z /\ forall z', Good z' -> z' = z}.
Proof. (* ... *) Qed.
Что касается вашего второго вопроса, то да, это немного связано с первой точкой. Еще раз, я бы рекомендовал записать функцию y_from_x с типом Z -> Z, которая будет вычислять y с учетом x, а затем отдельно доказать, что эта функция связывает входы и выходы определенным образом. Тогда вы можете сказать, что y s различны для разных x s, доказав, что y_from_x является инъективным.
С другой стороны, я не уверен, как ваш последний пример относится к этому второму вопросу. Если я понимаю, что вы хотите сделать правильно, то вы можете написать что-то вроде
Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) :=
exists zs : list Z,
Z.of_nat (length zs) = N
/\ NoDup zs
/\ Forall IsGood zs.
Здесь Z.of_nat : nat -> Z канонических инъекций от натуралов до целых чисел, NoDup предикат утверждает, что список не содержит повторяющиеся элементы, и Forall - предикат более высокого порядка, утверждающий, что данный предикат (в данном случае IsGood) содержит все элементы списка.
В заключение я бы посоветовал использовать Z для вещей, которые могут включать только натуральные числа. В вашем примере вы используете целое число, чтобы говорить о мощности набора, и это число всегда является натуральным числом.