Real number without axiom

Hello everyone.

I composed real number without using any axioms other than that of logic. Is this useful for the community?

I’m not a specialist, but are you aware that since Coq 8.11, the real numbers from Coq’s standard library are based on just three logical axioms (see

If you are interested to contribute to this kind of topics, the relevant people to talk to are Vincent Semeria (@VincentSe on GitHub) and the other reals library maintainers in the Coq standard library (@silene, @MSoegtropIMC, @herbelin, @lthery). Other related works outside of the standard library include CoRN (, which is maintained by Vincent and @spitters, and (by @affeldt, @CohenCyril, @amahboubi and others).

1 Like

Hello @itleigns, welcome to the Coq community!

It’s indeed a great place to share code and developments (and quite a few people are interested in reals as shown by the previous post), however you should probably be a bit careful with statements like

It’s true that all the axioms that you are using come from the standard library but they are far from innocuous: combining excluded middle with indefinite description as you are doing in your development is assuming almost the strongest axioms people are usually considering in this community.

Of course, I don’t mean to belittle this approach (it’s perfectly fine to do classical mathematics and I think math-comp/analysis takes a similar set of axioms for good reasons — you should really check it out if that’s a topic you are interested in), nor your development, just to gently warn you that your wording might be misinterpreted in this context.

Thank you for the information!
I was not aware of the real numbers based on just three logical axioms.

I will see CoRN because I am interested in analysis.

Thank you for your advice.
Could you please let me know how I should have worded it in this case?

I guess I would say something like “only axioms coming from the standard library”. When I first read your phrase I (mis)interpreted it as “no axioms at all besides the ones underlying Coq’s logic” which is a bit different.

1 Like

Thank you.
I’ve learned a lot. I’ll be careful from now on.

Note that fourcolor also has it’s own implementation of real numbers using only a strong form of EM [IIAC]

Vincent Semeria is working hard on integrating corn and math-classes with the (constructive) stdlib reals.
This is part of a bigger effort to coordinate some of the work on real numbers.