Stream: math-comp users

Topic: Ring does not update its operations


view this post on Zulip Laura Brædder (Jun 26 2023 at 13:26):

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!

view this post on Zulip Paolo Giarrusso (Jun 26 2023 at 17:47):

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

view this post on Zulip Paolo Giarrusso (Jun 26 2023 at 17:48):

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

view this post on Zulip Cyril Cohen (Jun 26 2023 at 18:03):

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 ...

view this post on Zulip Laura Brædder (Jun 29 2023 at 06:45):

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

view this post on Zulip Bas Spitters (Jun 29 2023 at 07:04):

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.

view this post on Zulip Ana de Almeida Borges (Jun 29 2023 at 09:40):

Yes! There is also FV Prim63 to MathComp from here, but it focuses on primitive integers

view this post on Zulip Pierre Roux (Jun 29 2023 at 11:11):

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

view this post on Zulip Karl Palmskog (Jun 29 2023 at 14:20):

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

view this post on Zulip Bas Spitters (Jun 29 2023 at 14:57):

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

view this post on Zulip Karl Palmskog (Jun 29 2023 at 14:59):

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.

view this post on Zulip Kazuhiko Sakaguchi (Jun 29 2023 at 19:31):

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.

view this post on Zulip Kazuhiko Sakaguchi (Jun 29 2023 at 19:37):

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.

view this post on Zulip Bas Spitters (Jun 29 2023 at 19:38):

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

view this post on Zulip Karl Palmskog (Jun 29 2023 at 19:46):

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

view this post on Zulip Bas Spitters (Jun 30 2023 at 07:45):

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...

view this post on Zulip Karl Palmskog (Jun 30 2023 at 07:49):

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

view this post on Zulip Kazuhiko Sakaguchi (Jun 30 2023 at 09:36):

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