Turning "exists unique" into a function in Coq

Using Coq
#1

Take something like the least upper bound property of the reals. Suppose I assume this axiom, suitably expressed in Coq’s logic, i.e. forall S subset of reals, if S is non-empty and exists x such that x is an upper bound on S, then there exists z such that z is an upper bound and if a is also an upper bound, a >= z."

So this means I can create a function, called supremum, from S to least upper bound of S. In Coq, given an axiom / assumption / theorem like that, how can I then use it to create a function, presumably a FixedPoint? Supremum is just an example, in many places in math we say “given S there exists unique x such that…”, and this let’s you talk about a function of S. How do I do that in Coq? Another example in the sqrt() function for any positive real.

#2

That is too vague as a question. It really depends on how your supremum is axiomatized and what other axioms you have at hand. Fox example, if you define the supremum as follows:

Axiom sup: forall S: R -> Prop, {v:R | forall x, S x -> (forall y, S y -> y <= v) /\ (forall x, (forall y, S y -> y <= x) -> v <= x) }.

then the answer to your question is trivial: sup is already a function.

You can have a look at the Coquelicot library to see how the completeness axiom from Coq’s standard library is turned into a function Rbar_lub.

#3

Thanks a lot! Is there an introduction to Coq where I can learn more about this? I read vol 1 of Software Foundations, i.e. Logical Foundations, but it didn’t seem to cover things like how your sup Axiom is also a function.

Also, coquelicot.saclay.inria.fr seems to be down.

#4

One can also use the axiom of constructive_indefinite_description.

The lemma of functional_choice follows.