Hello everyone.

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

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.