Hello everyone.
I composed real number without using any axioms other than that of logic. Is this useful for the community?
1 Like
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.
1 Like
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.
1 Like
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.