Coq Reals 和 Ssreflect GRings

Question

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

例如，我希望能够直接对 Rdefintions.R 类型的变量使用为 ssralg.GRing.Ring 定义的 add、mul 等操作并将 Num.real_closed_axiom 直接应用于 Coq 实数。

是否需要证明从eqType、choice、zmodule等到ClosedReals的所有结构？如果是这样，那么以前肯定有人这样做过，但我一直没能找到。我可以使用其他开发吗？

如果不是这样，那么通过公理实现它的正确方法是什么？是否必须添加额外的强制转换和 Canonical 结构语句。

Answer 1

Anton 的回答是正确的，这个问题在最近的 MathComp 会议上进行了讨论，"official" 可以在 https://github.com/math-comp/analysis/blob/master/Rstruct.v

上找到 Coq 实数的实验绑定

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