search

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

RingOrder for types with decidable equality #99

Open mdgeorge4153 opened 3 years ago

mdgeorge4153 commented 3 years ago

I'm interested in working with ordered rings with decidable equality (in particular, I would like to show that the field of fractions of an ordered ring is also ordered in the natural way, and that an ordered commutative ring is an integral domain).

As noted in the comments of interfaces/orders.v, the deeply nested class hierarchy for orders is difficult to work with. The comment says "we will, later on, provide means to go back and forth between the usual classical notions and these constructive notions." but I can't tell whether this connection has been done or how to use it if it has.

Apologies if this is an inappropriate place to ask.

spitters commented 3 years ago

I don't think that has been done, so a PR would be welcome.

mdgeorge4153 commented 3 years ago

Sounds good. I'm still a bit new to Coq, but I'll see what I can do.