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.
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.
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.