Stream: math-comp users

Topic: Problem with exports in ssralg.v


view this post on Zulip Laura Brædder (Jun 21 2023 at 09:31):

Hi, I'm trying to prove that a field in the standard library is also a field in math-comp, i.e. has fieldType. I'm able to show that it is a group using ZmodMixin. However, when I want to show that it is also a ring, I can't find the exports to do so. I wanted to use something like GRing.Zmodule_isComRing.Build (when I use this, Coq claims that it is not in the current environment even if I have imported GRing.Theory and opened a local ring_scope... (it may be where my problem lies I don't know)) but cannot seem to find the right commands to do so. Is there missing some exports, or am I misunderstanding how things work?
Also, in the export sections, there are a lot of .clone, and I do not understand the purpose of these. Are they from Hierarchy Builder?
Any ideas as to where I might go wrong? Thanks!

view this post on Zulip Cyril Cohen (Jun 21 2023 at 09:33):

Hi! and welcome. Did you do From mathcomp Require Import ssralg ? Can you provide a link to the coq code? The purpose of .clone is to recover the structure from a given type, from coq 8.16 they may actually have no use anymore.

view this post on Zulip Laura Brædder (Jun 21 2023 at 09:43):

Thank you! Yes, I have that piece of code. Here is my code so far: https://github.com/AU-COBRA/OVN/blob/equivalence/theories/Main.v (A little heads up: It is not a very pretty code...)
Oh okay, but then why is it enough to only export .clone?

view this post on Zulip Cyril Cohen (Jun 21 2023 at 09:52):

I'm not sure I understand the question. The only purpose of export is to get notation in the global scope or shorter names. .clone are available without exports, the purpose of the .clone in export modules is to make the notations from mathcomp 1 available, but they will disappear in later versions.

view this post on Zulip Laura Brædder (Jun 21 2023 at 09:54):

That makes sense. Thank you for clearing that for me.

view this post on Zulip Laura Brædder (Jun 21 2023 at 12:56):

However, I still don’t understand why my code will not work…

view this post on Zulip Pierre Roux (Jun 21 2023 at 13:21):

If you do HB.about GRing.Zmodule_isComRing.Build. it tells that you need R to be a Zmodule so you need to use GRing.isZmodule.Build and in turns HB.about GRing.isZmodule.Build tells that we need R to be a choiceType. If you are doing classical logic, using From mathcomp Require Import boolp from the hierarchy-builder branch of MathComp Analysis, one can do the following

From mathcomp Require Import boolp.
<your code>
HB.instance Definition _ := Choice.copy R {classic R}.
HB.instance Definition _ := GRing.isZmodule.Build R raddA raddC rO_id ropp_inverse.
<your code>
Lemma rInotrO': rI != 0%R. Proof. R_is_field. apply/eqP/F_1_neq_0. Qed.
HB.instance Definition _ := GRing.Zmodule_isComRing.Build R rmulA rmulC rI_left_id
   left_dist_rmul_radd rInotrO'.

view this post on Zulip Laura Brædder (Jun 22 2023 at 09:30):

Great, thank you so much! Now, I seems to be missing a package or something like that because when I try to run a simple program such as the following:

From elpi Require Import elpi.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require ssralg ssrnum zmodp. (* all_algebra *)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Groups.

Import ssralg GRing.Theory.
Local Open Scope ring_scope.

HB.about GRing.isZmodule.Build.

End Groups.

I get the error: Error: HB: unable to locate GRing.isZmodule.Build. Does anyone see what is wrong? Also, do you know if there is somewhere that has a lot of documentation on this stuff?

view this post on Zulip Karl Palmskog (Jun 22 2023 at 09:41):

not sure if it covers exactly what you want, but there are a lot MathComp specific resources listed here: https://github.com/coq-community/awesome-coq#resources

view this post on Zulip Cyril Cohen (Jun 22 2023 at 09:49):

Laura Brædder said:

Great, thank you so much! Now, I seems to be missing a package or something like that because when I try to run a simple program such as the following:

From elpi Require Import elpi.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require ssralg ssrnum zmodp. (* all_algebra *)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Groups.

Import ssralg GRing.Theory.
Local Open Scope ring_scope.

HB.about GRing.isZmodule.Build.

End Groups.

I get the error: Error: HB: unable to locate GRing.isZmodule.Build. Does anyone see what is wrong? Also, do you know if there is somewhere that has a lot of documentation on this stuff?

About HB.about this is certainly a bug.... please file a bug report.
As for documentation, here is the documentation of HB:
https://github.com/math-comp/hierarchy-builder/tree/master#documentation
This is work in progress.

view this post on Zulip Pierre Roux (Jun 22 2023 at 10:02):

Laura Brædder said:

I get the error: Error: HB: unable to locate GRing.isZmodule.Build. Does anyone see what is wrong? Also, do you know if there is somewhere that has a lot of documentation on this stuff?

Strange, this works fine here with the Opam package coq-mathcomp-algebra.2.0.0

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

Ah, that might be the problem. I'm only working with coq-mathcomp-algebra.1.16.0 since another package used in the code in trying to make needs to run in a version of Coq between 8.16 and strictly below 8.17 so I'm using Coq8.16.1...

view this post on Zulip Karl Palmskog (Jun 22 2023 at 10:27):

MathComp 2.0.0 works with Coq 8.16.

view this post on Zulip Laura Brædder (Jun 22 2023 at 10:28):

Perfect! Then I just need to update it and everything should be fine. Thank you guys so much :smiley:

view this post on Zulip Bas Spitters (Jun 22 2023 at 11:18):

We are currently waiting for the porting of extructures and deriving to mathcomp 2.0.
https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/SSProve.20in.20MC.20CI.3F
https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Porting.20Deriving.20to.20math-comp.202.2E0.2E0

Would there be an intermediate version we can use?

view this post on Zulip Cyril Cohen (Jun 22 2023 at 11:35):

@Bas Spitters I believe this message belongs to a different topic? Which one? You are intermediate version of which softaware/library?

view this post on Zulip Bas Spitters (Jun 22 2023 at 11:39):

Hi @Cyril Cohen , Laura is working with SSProve, so I expect that she cannot just update to MC2.0.

view this post on Zulip Bas Spitters (Jun 22 2023 at 11:40):

For context, Laura has just started as my PhD-student on a project on verified voting protocols.
https://direc.dk/verified-voting-protocols-and-blockchains/

view this post on Zulip Cyril Cohen (Jun 22 2023 at 11:54):

Then I'm a bit lost ... Are you asking whether you can use mathcomp 1.17? Maybe you could tell us what are the features you require?

view this post on Zulip Kazuhiko Sakaguchi (Jun 22 2023 at 12:31):

@Bas Spitters If you plan to use Algebra Tactics (I guess it from your recent questions), note that porting Algebra Tactics to MathComp 2.0 takes some more time. https://github.com/math-comp/algebra-tactics/pull/71

view this post on Zulip Paolo Giarrusso (Jun 22 2023 at 13:02):

@Bas Spitters @Laura Brædder HB.about GRing.isZmodule.Build. would only make sense if GRing.isZmodule.Build were defined with hierarchy-builder, but mathcomp 1 never uses HB

view this post on Zulip Paolo Giarrusso (Jun 22 2023 at 17:11):

as an outsider, your options seem (a) move to math-comp 2 (b) stop using HB and do everything in the older (more complex?) way (3) _maybe_ you can mix math-comp 1 with HB for separate structures that don't interact with MC, but I'm skeptical


Last updated: Jul 15 2024 at 20:02 UTC