Hi there, sorry for spamming you... Bear in mind through the following that I'm using the old version of mathcomp. I'm still working on showing that a field in the standard library can be implemented in the mathcomp library. To do this, I've shown that a choiceType R which is assumed to be a field in the standard library, is an abelian group (zmodType), a ring and, furthermore, a commutative ring (ringType and comRingType) and a unit ring (comUnitRingType). I need to show that R is also an integral domain. To do so, I initially just showed the axiom directly with my ring operations, but when I then tried to make R into an IdomainType, Coq told me that I needed to use `GRing.Idomain.axoim (GRing.Ring.Pack ?b0)`

, which I interpret as meaning `GRing.Idomain.axoim R_RingType`

where `R_RingType`

is the original `R`

from the beginning but supposedly with the ring operations defined throughout the code. However, when I try to prove this, i.e. to prove `GRing.Idomain.axoim R_RingType`

, the ring operations Coq is working with are not the same as the ring operations that I defined, and I cannot figure out why. I don't understand where my ring operations have gone if they are not "attached" to my ring.

I would have liked to give you a short example of my problem, but I think that without having first to show that R is a group, a ring, and a unit ring, the problem loses some of its meaning. So if anyone wants to take a look at my code, it is available here: https://github.com/AU-COBRA/OVN/blob/equivalence/theories/Main.v

Thanks!

where do things fail, and what are the definitions? I only see `Variables`

in your link:

```
Variable R : choiceType.
(* We need to assume R has choiceType. This is a reasonable assumption as we are working
with finite fields and one can prove Choice for countable types so in particular for
finite types. *)
Variable (rO rI : R) (radd rmul rsub: R -> R -> R) (ropp : R -> R).
Variable (rdiv : R -> R -> R) (rinv : R -> R).
```

I'm trying to install this over `__coq-platform.2022.09.0~8.16.0~2022.09~beta1`

(mathcomp 1) + ssprove, but curious about the deps

(also I'm not a math-comp expert)

I didn't look into it enough, but my guess is that you are unfortunately confronted with the absence of eta for structures in the mathcomp hierarchy. I suggest you postulate an `eqMixin`

and a `choiceMixin`

and start a section `FieldEquivalence`

like this

```
Module FieldEquivalence.
Section FieldEquivalence
Require Import Setoid.
Variables (R : Type) (ReqMixin : Equality.mixin_of R) (RchoiceMixin : Choice.mixin_of R).
Canonical R_eqType := EqType R ReqMixin.
Canonical R_choiceType := ChoiceType R RchoiceMixin.
```

NB: I advocate for the creation of a section in order to abstract over `R `

rather than postulating the existance of a constant ...

Thank you so much for the help. It is working now!

Would there be an interest in having such a connection between stdlib and mc in a more central place?

Perhaps in connection with the algebra tactics by @Kazuhiko Sakaguchi

I know mczify makes similar connections too.

Yes! There is also `FV Prim63 to MathComp`

from here, but it focuses on primitive integers

Also a link with Reals from the stdlib in Analysis (Rstruct.v file)

(warning that an MIT-licensed project can't include non-commercial-use licensed code)

@Karl Palmskog I think I understand where you are going but can you be explicit about what cannot include what?

unless I'm missing something, the code Ana is alluding to here is licensed under a noncommercial license, while the project Laura is working on is using MIT.

Ideally, I rather want to give a cleaner reimplementation of sparse Horner forms following the refinement approach, so that I don't have to reuse `setoid_ring`

in Algebra Tactics. It was just a shortcut to make it work.

I guess that a typical motivation for combining stuff from the Coq standard library and MathComp is performance. Then, what you need is refinements. The right place to collect such refinements would be something like CoqEAL.

A reason for combining with the stdlib is when one has two code bases with different dependencies :-)

I agree in general that CoqEAL is the best place for any connections between Stdlib and MathComp

Coqeal has quite a few dependencies. https://github.com/coq-community/coqeal

I'm a bit afraid of dragging in even more in our project...

ah, dependency aversion! At least all those deps are in the Platform. I don't think we can simultaneously have a sparse dep graph and have good ecosystem growth, unfortunately

Paramcoq is essential for refinements. Without MathComp algebra, we cannot even talk about integers on the MathComp side. But, it might be possible to split CoqEAL into several packages, so that the minimal requirement of using CoqEAL becomes these two packages.

Last updated: Jul 15 2024 at 19:01 UTC