Stream: math-comp users

Topic: comSemiRing with bool


view this post on Zulip Julin Shaji (Oct 13 2023 at 11:39):

I want to make a commutative semiring with bool as type.

What should be done to make such a ring?

I guess I need to use a mixin? If so, which one should I use?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 13 2023 at 12:23):

I'm talking about math-comp 1 (still didn't upgrade to 2, but I guess it is similar). For that the right type was comRingType, which requires the corresponding mixin; I think.

However, math-comp already has an instance for bool, so you need to do nothing!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 13 2023 at 12:24):

bool_comRingType

view this post on Zulip Emilio Jesús Gallego Arias (Oct 13 2023 at 12:25):

I think this is exactly what you were looking for.

view this post on Zulip Julin Shaji (Oct 13 2023 at 17:02):

Isn't there a way to make a semiring?

I couldn't find a mixin for semiring in the docs.

Could it be that there is some other way? Or am I just not looking at the right place?

I was trying to make a commutative semiring from option bool this time.

view this post on Zulip Pierre Roux (Oct 13 2023 at 17:16):

https://github.com/math-comp/math-comp/blob/122b27068cbdaa662c2c90cac259e452133f9f34/mathcomp/algebra/ssralg.v#L21-L23
(math-comp 2 only)

view this post on Zulip Julin Shaji (Oct 14 2023 at 03:46):

Oh, it's not there in mathcomp-1, is it?

view this post on Zulip Julin Shaji (Oct 14 2023 at 03:51):

I suppose that's the case.

Docs for v1 doesn't seem to mention semiRingType but docs for v2 does.

view this post on Zulip Julin Shaji (Oct 14 2023 at 03:56):

I think I had been using mathcomp-1 while looking at the documentation of mathcomp-2.. :woozy_face:

view this post on Zulip Julin Shaji (Oct 14 2023 at 04:24):

How can we make a comSemiRing in mathcomp-1?

Found this: https://gist.github.com/pi8027/58e56d2383e2ca94051bc6f4cbf37d24

Would something like this be okay?
I wasn't sure if that gist was meant just to demo inner working of mathcomp or anything.

view this post on Zulip Julin Shaji (Oct 14 2023 at 05:29):

Is there a way to know which version of mathcomp we are using from inside the editor? Some command or variable which we can see?

view this post on Zulip Julin Shaji (Oct 14 2023 at 05:45):

Tried installing mathcomp2 from opam (been using mathcomp1 from nix so far), but couldn't get some imports to work.
So I was wondering if there is some version conflict.

For example, the second line in

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra.

gives

Error: Cannot find a physical path bound to logical path all_algebra with prefix mathcomp.

I wasn't sure if the HB import is needed, but put it there for good measure.

view this post on Zulip Paolo Giarrusso (Oct 14 2023 at 07:20):

You might not have installed enough math-comp packages

view this post on Zulip Pierre Roux (Oct 14 2023 at 09:06):

Julin Shaji said:

How can we make a comSemiRing in mathcomp-1?

you can't

view this post on Zulip Julin Shaji (Oct 14 2023 at 09:10):

Oh..

view this post on Zulip Pierre Roux (Oct 14 2023 at 09:12):

Well, easing the addition of structures like semirings is the whole purpose of mathcomp 2.

view this post on Zulip Paolo Giarrusso (Oct 14 2023 at 11:01):

You also need coq-mathcomp-algebra to load all_algebra / ssralg

view this post on Zulip Julin Shaji (Oct 15 2023 at 16:30):

I got mathcomp2 installed.

How can we make a type comSemiRing there? I wasn't sure where to look at, but I guess it involves the use of HB?

view this post on Zulip Pierre Roux (Oct 15 2023 at 16:38):

https://github.com/math-comp/math-comp/blob/master/etc/porting_to_mathcomp2/porting.pdf (we should link it in the README, not just on the wiki indeed)

view this post on Zulip Julin Shaji (Oct 16 2023 at 09:45):

Emilio Jesús Gallego Arias said:

bool_comRingType

Is bool_comRingType something predefined in mathcomp? I couldn't find it.

view this post on Zulip Cyril Cohen (Oct 16 2023 at 10:07):

One should not rely on a particular name from it but let Coq find the structure through bool : comRingType (if it exists). With mathcomp2 you may ask what structure is on bool via HB.about bool.

view this post on Zulip Julin Shaji (Oct 16 2023 at 12:16):

I had been trying to replicate whatever was done to make bool a semiring to get a comSemiRing out of option bool.

But I still can't get a handle on it.

I did:

HB.about comSemiRingType.
(*
HB: GRing.ComSemiRing is a factory for the following mixins:
    - GRing.isNmodule
    - hasChoice
    - hasDecEq
    - GRing.Nmodule_isSemiRing
    - GRing.SemiRing_hasCommutativeMul (* new, not from inheritance *)
 *)

and figured that one of the first things that needs be done for that is to define DecEq for option bool.

HB.about hasDecEq.
(*
HB: hasDecEq is a factory (from "./ssreflect/eqtype.v", line 135)

HB: hasDecEq operations and axioms are:
    - eq_op
    - eqP

HB: hasDecEq requires the following mixins:

HB: hasDecEq provides the following mixins:
    - hasDecEq
*)

I suppose we need to use the mixin named hasDecEq? The structure for this seems to be Equality (or is it something else?).

Lemma oB_comparable: comparable (option bool).
Proof.  do !case; by [left | right].  Qed.

Definition oB_compareb (x y: option bool): bool := oB_comparable x y.

Lemma oB_compareP: Equality.axiom oB_compareb.
Proof.  move=> x y; apply: sumboolP.  Qed.

HB.instance Definition oB_hasDecEq: hasDecEq (option bool) :=
  hasDecEq.Build (option bool) oB_compareP.

How can I make option bool an eqType?

Am I headed in the right direction to make option bool a comSemiRing?

view this post on Zulip Julin Shaji (Oct 16 2023 at 12:19):


Oh, option itself has eqtype.Equality structure. That combined with that of bool can make the same for option bool as well?
(but how though..)

And is HB.about not meant to work for types like option bool?

view this post on Zulip Paolo Giarrusso (Oct 16 2023 at 12:34):

Re "how?", equality for option A will need equality for A

view this post on Zulip Enrico Tassi (Oct 16 2023 at 12:34):

Look at what we do for list:
https://github.com/math-comp/math-comp/blob/122b27068cbdaa662c2c90cac259e452133f9f34/mathcomp/ssreflect/seq.v#L1053
you want the instance to talk about option X for any X which is an eqType.

view this post on Zulip Paolo Giarrusso (Oct 16 2023 at 12:34):

"you want"? That's done already right?

view this post on Zulip Enrico Tassi (Oct 16 2023 at 12:35):

Note that there is already an eqType for option, so your command may have no effect if you have MC2.0 loaded.

view this post on Zulip Julin Shaji (Oct 16 2023 at 12:40):

Paolo Giarrusso said:

Re "how?", equality for option A will need equality for A

Yeah, but is there a way to do some kind of composing of structures or something? Or do we have to manually write the definitions each time?

I may be talking nonsense here, still only getting familiar with HB.

view this post on Zulip Enrico Tassi (Oct 16 2023 at 12:47):

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra.

HB.about option.

gives

HB: option is canonically equipped with structures:
    - Countable
      (from "./ssreflect/choice.v", line 649)
    - choice.Choice
      (from "./ssreflect/choice.v", line 482)
    - eqtype.Equality
      (from "./ssreflect/eqtype.v", line 859)
    - fintype.Finite
      (from "./ssreflect/fintype.v", line 1423)

view this post on Zulip Enrico Tassi (Oct 16 2023 at 12:48):

So you don't need the mixins for these structures, but the other ones (isNmodule, nmodule_isSemiRing, ...)

view this post on Zulip Enrico Tassi (Oct 16 2023 at 12:50):

See also HB.howto bool comSemiRingType, which says:

HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
    - GRing.isNmodule; GRing.Nmodule_isComSemiRing
    - GRing.isSemiRing; GRing.SemiRing_hasCommutativeMul
    - GRing.isNmodule; GRing.Nmodule_isSemiRing;
      GRing.SemiRing_hasCommutativeMul

view this post on Zulip Enrico Tassi (Oct 16 2023 at 12:51):

The last solution is the one I was suggesting, but you have shorter factories. You need to have an HB.instance for each of the factories in one of the 3 solutions

view this post on Zulip Julin Shaji (Oct 16 2023 at 13:46):

Thanks! Hadn't known about HB.howto. That's definitely handy.

view this post on Zulip Julin Shaji (Oct 16 2023 at 14:20):

I was trying to make an nmodType and the output of HB.about nmodType seemed to suggest that a add0r is needed.

What is add0r? Doing about and Check gave error.

Is it add 0 r = r?

In ssreflect, right_zero is mentioned. This is not it, right?

view this post on Zulip Pierre Roux (Oct 16 2023 at 14:29):

Once you've chose a factory (as suggested by HB.howto), you can use (as explained in HB.howto output) HB.about factory.Build (for instance HB.about GRing.isNmodule.Build) to see what arguments the factory is expecting.

view this post on Zulip Julin Shaji (Oct 16 2023 at 15:53):

Enrico Tassi said:

The last solution is the one I was suggesting, but you have shorter factories. You need to have an HB.instance for each of the factories in one of the 3 solutions

Each of these paths will deliver the same result, right? Would there be any difference?

view this post on Zulip Julin Shaji (Oct 16 2023 at 15:54):

Pierre Roux said:

Once you've chose a factory (as suggested by HB.howto), you can use (as explained in HB.howto output) HB.about factory.Build

Sorry, had neglected the Use 'HB.about F.Build' to see the arguments of each factory F) part in the message produced from Coq.

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:03):

Enrico Tassi said:

Look at what we do for list:
https://github.com/math-comp/math-comp/blob/122b27068cbdaa662c2c90cac259e452133f9f34/mathcomp/ssreflect/seq.v#L1053
you want the instance to talk about option X for any X which is an eqType.

I want to have this structure only for option bool and bool already has eqType. Would that work?

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:05):


This is what I got now (with errors):

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra.

Local Open Scope ring_scope.

Module b3.
  Definition t: Type := option bool.
  Definition one: t := Some true.
  Definition zero: t := Some false.
  Definition add (a b: t): t :=
    match a, b with
    | Some true, _ => Some true
    | _, Some true => Some true
    | Some false, Some false => Some false
    | _, _ => None
    end.
  Definition mul (a b: t): t :=
    match a, b with
    | Some false, _ => Some false
    | _, Some false => Some false
    | Some true, Some true => Some true
    | _, _ => None
    end.

  Lemma addrC: commutative add.
  Proof. by do !case. Qed.
  Lemma addrA: associative add.
  Proof. by do !case. Qed.
  Lemma add0r: left_id zero add.
  Proof. by do !case. Qed.
  Lemma mulrC: commutative mul.
  Proof. by do !case. Qed.
  Lemma mulrA: associative mul.
  Proof. by do !case. Qed.
  Lemma mul1r: left_id one mul.
  Proof. by do !case. Qed.
  Lemma mulrDl: left_distributive mul add.
  Proof. by do !case. Qed.
  Lemma mul0r: left_zero zero mul.
  Proof. by do !case. Qed.
  Lemma oner_neq0: is_true (one != zero).
  Proof. by []. Qed.
End b3.

HB.instance Definition _ := GRing.isNmodule.Build b3.t b3.addrA b3.addrC b3.add0r.

HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build
  b3.t b3.mulrA b3.mulrC b3.mul1r b3.mulrDl b3.mul0r b3.oner_neq0.
(*
Definition illtyped: The term "id_phant" has type "phantom Type b3.t -> phantom Type b3.t"
while it is expected to have type
 "unify Type Type b3.t ?t (is_not_canonically_a nmodType)".
*)

Is it saying that the type is not Nmodule? But then isn't the first HB.instance saying that it is an Nmodule?
What could be going wrong here?

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:06):

And don't the instances of the structures need names?
Like in the case of seq where an underscore is used: HB.instance Definition _ := hasDecEq.Build (seq T) eqseqP.

view this post on Zulip Enrico Tassi (Oct 16 2023 at 16:11):

weird. try #[verbose] HB.instance Definition _ := GRing.isNmodule.Build b3.t b3.addrA b3.addrC b3.add0r.

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:11):

Is the The term "id_phant" has type "phantom Type b3.t -> phantom Type b3.t"error because of using option bool instead of option?

HB.about (option bool) didn't go through either.

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:12):


Enrico Tassi said:

weird. try #[verbose] HB.instance Definition _ := GRing.isNmodule.Build b3.t b3.addrA b3.addrC b3.add0r.

I got this:

HB: skipping section opening

HB_unnamed_factory_13 is defined

[1697472740.840821] HB:  declare canonical mixin instance
«HB_unnamed_factory_13»

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:13):

Enrico Tassi said:

could you try with all axioms or box it?

:grimacing:
I don't know what either of those mean..

Does all axiom mean just the type without the definitions?

view this post on Zulip Enrico Tassi (Oct 16 2023 at 16:14):

nevermind, I think I was wrong

view this post on Zulip Julin Shaji (Oct 16 2023 at 16:21):

Got the same error upon trying for a GRing.Nmodule_isSemiRing as well..

HB.instance Definition _ := GRing.Nmodule_isSemiRing.Build b3.t b3.mulrA b3.mul1r b3.mulr1 b3.mulrDl b3.mulrDr b3.mul0r b3.mulr0 b3.oner_neq0.
(*
Definition illtyped: The term "id_phant" has type "phantom Type b3.t -> phantom Type b3.t"
while it is expected to have type
 "unify Type Type b3.t ?t (is_not_canonically_a nmodType)".
*)

view this post on Zulip Julin Shaji (Oct 17 2023 at 05:06):

Is there a way to get mathcomp2 and HB in jscoq over at https://coq.vercel.app/ ?

Wanted to see if the same error pops up in other computers as well.

view this post on Zulip Cyril Cohen (Oct 17 2023 at 07:15):

@Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 13:31):

I'm unsure, @Shachar Itzhaky did work on having elpi + hb running, but I don't know the status of that.

view this post on Zulip Julin Shaji (Oct 18 2023 at 06:32):

Enrico Tassi said:

weird. try #[verbose] HB.instance Definition _ := GRing.isNmodule.Build b3.t b3.addrA b3.addrC b3.add0r.

I guess this is not a bug as it's something elementary. Would opening an issue in the mathcomp repo with this query be a good idea?

view this post on Zulip Cyril Cohen (Oct 18 2023 at 08:00):

Emilio Jesús Gallego Arias said:

I'm unsure, Shachar Itzhaky did work on having elpi + hb running, but I don't know the status of that.

FTR @Enrico Tassi made it work for the last mathcomp school we had

view this post on Zulip Cyril Cohen (Oct 18 2023 at 08:03):

Julin Shaji said:

HB.instance Definition _ := GRing.isNmodule.Build b3.t b3.addrA b3.addrC b3.add0r.

HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build
  b3.t b3.mulrA b3.mulrC b3.mul1r b3.mulrDl b3.mul0r b3.oner_neq0.
(*
Definition illtyped: The term "id_phant" has type "phantom Type b3.t -> phantom Type b3.t"
while it is expected to have type
 "unify Type Type b3.t ?t (is_not_canonically_a nmodType)".
*)

Is it saying that the type is not Nmodule? But then isn't the first HB.instance saying that it is an Nmodule?
What could be going wrong here?

The problem here is that b3.t is not a choice type, although it is defined as an option of it.
You can do the following before the NModule declaration.

HB.instance Definition _ := Choice.on b3.t.

You could have seen it by typing: HB.howto b3.t NModule.type.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:39):

Cyril Cohen said:

FTR Enrico Tassi made it work for the last mathcomp school we had

I think indeed it should be easy to have it work then by default now; there was a bug in coqdep that was blocking the build, but Rodolphe was very kind to submit a fix. I don't have the cycles myself to do it, but if someone wants to do it I'm happy to help, please open a thread in the jsCoq stream so Shachar sees it. Basically what we need to do is to have the coq-elpi addon built by default on the webpage repository, which is what is deployed on vercel.

view this post on Zulip Enrico Tassi (Oct 18 2023 at 21:29):

I did work around build problems using make.
Another big problem was that the mathcomp package is incomplete, some parts are disabled with a patch. And that breaks mczify, which is required by algebra-tactics.

view this post on Zulip Julin Shaji (Oct 19 2023 at 06:34):

Cyril Cohen said:

The problem here is that b3.t is not a choice type, although it is defined as an option of it.
You can do the following before the NModule declaration.

HB.instance Definition _ := Choice.on b3.t.

You could have seen it by typing: HB.howto b3.t NModule.type.

:sweat: :sweat_smile:
Thanks.

view this post on Zulip djao (Oct 21 2023 at 03:43):

For summary purposes.

Set Warnings "-ambiguous-paths,-notation-overridden,
    -redundant-canonical-projection".
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg eqtype.
From Coq Require Import Utf8 Basics.
Set Bullet Behavior "Strict Subproofs".

Definition t: Type := option bool.
Definition one: t := Some true.
Definition zero: t := Some false.
Definition add (a b : t) : t :=
  match a, b with
  | Some true, _ => Some true
  | _, Some true => Some true
  | Some false, Some false => Some false
  | _, _ => None
  end.
Definition mul (a b : t) : t :=
  match a, b with
  | Some false, _ => Some false
  | _, Some false => Some false
  | Some true, Some true => Some true
  | _, _ => None
  end.

Lemma addrC: commutative add.
Proof. by do !case. Qed.
Lemma addrA: associative add.
Proof. by do !case. Qed.
Lemma add0r: left_id zero add.
Proof. by do !case. Qed.
Lemma mulrC: commutative mul.
Proof. by do !case. Qed.
Lemma mulrA: associative mul.
Proof. by do !case. Qed.
Lemma mul1r: left_id one mul.
Proof. by do !case. Qed.
Lemma mulrDl: left_distributive mul add.
Proof. by do !case. Qed.
Lemma mul0r: left_zero zero mul.
Proof. by do !case. Qed.
Lemma oner_neq0: is_true (one != zero).
Proof. by []. Qed.

HB.instance Definition _ := Choice.on t.
HB.instance Definition _ := GRing.isNmodule.Build t addrA addrC add0r.
HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build
                              t mulrA mulrC mul1r mulrDl mul0r oner_neq0.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2023 at 14:42):

Enrico Tassi said:

Another big problem was that the mathcomp package is incomplete, some parts are disabled with a patch. And that breaks mczify, which is required by algebra-tactics.

The patch we have is on ssrnat, basically we don't want ssrnat to import all of stdlib just for the binnat theorems, as this added huge network latency.

IMHO the patch can be easily upstreamed, I just didn't have the cycles to do it.

view this post on Zulip Pierre Roux (Oct 23 2023 at 14:48):

FWIW I have a branch of mathcomp that compiles without the stdlib (only the prelude), this may be similar: https://github.com/proux01/math-comp/tree/attempt_cut_stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2023 at 14:53):

That would also work great for jsCoq


Last updated: Jul 15 2024 at 20:02 UTC