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 https://coq.inria.fr/refman/changes.html#reals)?

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 (https://github.com/coq-community/corn), which is maintained by Vincent and @spitters, and https://github.com/math-comp/analysis (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.