Coq Reals and Ssreflect GRings

Question

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.

I haven't looked at it closely, but [math-comp/analysis](https://github.com/math-comp/analysis) might be relevant. — Anton Trunov, Apr 16 '18 at 17:08

ejgallego · Accepted Answer · 2018-04-16T23:18:51.020

3

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.

edited Apr 16 '18 at 23:18

answered Apr 16 '18 at 21:18

ejgallego

6,709
1
14
29

Thanks. Are there longer term plans for Coquelicot and ssreflect to integrate more closely? – larsr Apr 16 '18 at 21:35
I'm afraid I am not the right person to answer that question. – ejgallego Apr 16 '18 at 23:20

Coq Reals and Ssreflect GRings

1 Answers1