Search code examples
coqreal-numberssreflect

Coq Reals and Ssreflect GRings

I'd like to use ssreflect's lemmas on the Reals defined in Coq.Reals.Raxioms. How do I do that?

For example, I'd like to be able to use the add, mul, etc. operations defined for ssralg.GRing.Ring directly on variables of type Rdefintions.R and apply the Num.real_closed_axiom directly on Coq reals.

Is it necessary to prove all the structures from eqType, choice, zmodule, etc, up to the ClosedReals? If so, someone must have done so before, but I have not been able to find it. Is there some other development I can use?

If not so, what is the right way to do it via axioms? Does one have to add additional coercions and Canonical structure statements.

Solution

  • Anton's response is correct, this issue was discussed in a recent MathComp meeting, and an "official" experimental bindings to Coq's reals can be found at https://github.com/math-comp/analysis/blob/master/Rstruct.v

    Note that the above library is still in heavy development, I suggest you directly discuss with the developers for more information.