coq - Coq Reals 和 Ssreflect GRings

Question

我想在定义的 Reals 上使用 ssreflect 的引理Coq.Reals.Raxioms。我怎么做？

例如，我希望能够直接在类型变量上使用定义的add、mul等操作，并直接在 Coq 实数上应用。ssralg.GRing.RingRdefintions.RNum.real_closed_axiom

是否有必要证明从 eqType、choice、zmodule 等到 ClosedReals 的所有结构？如果是这样，之前一定有人这样做过，但我一直无法找到它。我可以使用其他一些开发吗？

如果不是这样，那么通过公理来做到这一点的正确方法是什么？是否必须添加额外的强制和Canonical结构语句。

Answer 1

Anton 的回答是正确的，这个问题在最近的 MathComp 会议上进行了讨论，可以在https://github.com/math-comp/analysis/blob/master/Rstruct.v找到与 Coq 实数的“官方”实验绑定

请注意，上述库仍在大力开发中，建议您直接与开发人员讨论以获取更多信息。