I want to make a commutative semiring with `bool`

as type.

- R: bool
- +: orb
- *: andb
- 1: true
- 0: false

What should be done to make such a ring?

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

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!

`bool_comRingType`

I think this is exactly what you were looking for.

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.

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

(math-comp 2 only)

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

I suppose that's the case.

Docs for v1 doesn't seem to mention `semiRingType`

but docs for v2 does.

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

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.

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?

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.

You might not have installed enough math-comp packages

Julin Shaji said:

How can we make a comSemiRing in mathcomp-1?

you can't

Oh..

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

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

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`

?

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)

Emilio Jesús Gallego Arias said:

`bool_comRingType`

Is `bool_comRingType`

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

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`

.

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?

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`

?

Re "how?", equality for `option A`

will need equality for `A`

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.

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

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

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.

```
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)
```

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

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

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

Thanks! Hadn't known about `HB.howto`

. That's definitely handy.

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?

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.

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?

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.

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?

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?

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

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

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.

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»
```

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?

nevermind, I think I was wrong

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)".
*)
```

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.

@Emilio Jesús Gallego Arias

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

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?

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

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`

.

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.

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.

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.

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

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.

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

That would also work great for jsCoq

Last updated: Jul 15 2024 at 20:02 UTC