Coq Reals和Ssreflect

Question

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

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

是否有必要证明所有的结构从eqType，选择，zmodule等，直到ClosedReals？如果是这样的话，一定有人这样做过，但我一直未能找到它。还有什么其他的开发我可以用吗？

如果不是这样的话，通过公理做这件事的正确方法是什么？是否必须添加额外的矫顽力和Canonical结构语句。

Answer 1

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

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