Definition by property in coq -

i having trouble formalizing definitions of following form: define integer such property holds.

let's formalized definition of property:

definition isgood (x : z) : prop := ... 

now need definition of form:

definition : z := ... 

assuming proved integer property exists , unique:

lemma lemma_goodexistsunique : exists! (x : z), isgood x. 

is there easy way of defining good using isgood , lemma_goodexistsunique?

since, property defined on integer numbers, seems no additional axioms should necessary. in event, don't see how adding axiom of choice can definition.

also, having trouble formalizing definitions of following form (i suspect related problem described above, please indicate if not case): every x, there exists y, , these y different different x. like, example, how define there n distinct integer numbers using isgood:

definition therearengoodintegers (n : z) (isgood : z -> prop) := ...? 

in real-world mathematics, definitions occur every , again, should not difficult formalize if coq intended suitable practical mathematics.

the short answer first question is: in general, not possible, in particular case, yes.

in coq's theory, propositions (i.e., props) , proofs have special status. in particular, in general not possible write choice operator extracts witness of existence proof. done make theory compatible axioms , principles, such proof irrelevance, says proofs of given proposition equal each other. if want able this, need add choice operator additional axiom theory, in standard library.

however, in particular cases, is possible extract witness out of abstract existence proof without recurring additional axioms. in particular, possible countable types (such z) when property in question decidable. can instance use choicetype interface in ssreflect library want (look xchoose function).

that being said, advice against doing things in style, because leads unnecessary complexity. easier define good directly, without resorting existence proof, , prove separately good has sought property.

definition : z := (* ... *) definition isgood (z : z) : prop := (* ... *)  lemma goodisgood : isgood good. proof. (* ... *) qed.  lemma goodunique : forall z : z, isgood z -> z = good. 

if absolutely want define good existence proof, can change proof of lemma_goodexistsunique use connective in type instead of prop, since allows extract witness directly using proj1_sig function:

lemma lemma_goodexistsunique : {z : z | z /\ forall z', z' -> z' = z}. proof. (* ... *) qed. 

as second question, yes, bit related first point. once again, recommend write down function y_from_x type z -> z compute y given x, , prove separately function relates inputs , outputs in particular way. then, can ys different different xs proving y_from_x injective.

on other hand, i'm not sure how last example relates second question. if understand want correctly, can write like

definition therearengoodintegers (n : z) (isgood : z -> prop) :=   exists zs : list z,     z.of_nat (length zs) = n     /\ nodup zs     /\ forall isgood zs. 

here, z.of_nat : nat -> z canonical injection naturals integers, nodup predicate asserting list doesn't contain repeated elements, , forall higher-order predicate asserting given predicate (in case, isgood) holds of elements of list.

as final note, advice against using z things can involve natural numbers. in example, using integer talk cardinality of set, , number natural number.