Trying out a simple chain of structures seems to fail with a strange error message:

```
Error:
parameter illtyped: In environment
A : indexed Type
The term "id_phant" has type
"phantom (indexed Type) A -> phantom (indexed Type) A"
while it is expected to have type
"unify (indexed Type) Type A ?t
(Some ("is not canonically a", Semigroup.type))".
```

How can I reorganize the Semigroup <: Monoid <: Group hierarchy for this to work?

```
From HB Require Import structures.
From Coq Require Import ssreflect ZArith.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall x y z, add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
HB.mixin Record IsMonoid A of IsSemigroup A := {
zero : A;
add0r : forall x, add zero x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
Infix "+" := add.
Check forall (M : Monoid.type) (x : M), x + x = 0.
HB.mixin Record IsGroup A of IsMonoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
```

It seems the same "bug" of https://github.com/math-comp/hierarchy-builder/issues/258.

The work around is to use `of Monoid A`

instead of `of IsMonoid A`

since the class (`Monoid`

) is closed transitively, but the mixin (`IsMonoid`

) is not, and you need all the dependency of `IsMonoid`

to state you axiom (you need `+`

which is in the semigroup.

or use `of IsMonoid A & IsSemigroup A`

, which is like using the class, but more verbose

we will eventually fix this annoyance

Enrico Tassi said:

or use

`of IsMonoid A & IsSemigroup A`

, which is like using the class, but more verbose

Ah I tried this but I get the same error

using `of Monoid A`

works, thanks, but I run into an error when I try to add commutativity into the mix:

Hum, ok, then please post your file so that I can try it myself.

Neither `IsGroup A`

or `Group A`

fixes the declaration of `IsComGroup`

```
From HB Require Import structures.
From Coq Require Import ssreflect ZArith.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall x y z, add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
HB.mixin Record IsMonoid A of IsSemigroup A := {
zero : A;
add0r : forall x, add zero x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
Infix "+" := add.
Check forall (M : Monoid.type) (x : M), x + x = 0.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of IsGroup A := {
addrC : forall x y, add x y = add y x;
}.
HB.structure Definition ComGroup := { A of IsComGroup A }.
```

as a side note I was reading chapter 8 of MCB and I can see why HB is a big improvement for the user :joy:, remembering OOP-style boilerplate is difficult

This is another problem, your axiom does not put `x`

nor `y`

in `A`

. If you add a type annotation it works.

```
addrC : forall x y : A, add x y = add y x;
```

Ah that works, thanks! How can I see the generated code by HB?

You can prefix any HB command with `#[log]`

or, if you are really brave, `#[log(raw)]`

.

But fasten you seat belt ;-)

You can also use `#[verbose]`

to get a more gentle listing of what is going on

Spotted some minor typos in Ch 8, PR coming :)

Thanks!

`Error: Attribute log is not supported`

I tried `#[log] HB.structure Definition Group := { A of IsGroup A }.`

Hum, it was added in version 1.1.0

which version are you on?

Ah 1.0.0 that's in Nixpkgs

You can `Print Module Group`

, but it does not print a lot of stuff

I have a PR bumping the version, hopefully @Cyril Cohen or @Vincent Laporte can review https://github.com/NixOS/nixpkgs/pull/130023

Like canonical structures etc

Ah 1.1.0 seems to cause a build failure in mathcomp-analysis

I see, this module looks identical to the one one would handwrite

Maybe mathcomp-analysis needs to be bumped also in Nixpkgs

```
File "./theories/measure.v", line 152, characters 0-276:
Warning: elpi: Using coq.env.add-const for declaring axioms or section
variables is deprecated. Use coq.env.add-axiom or
coq.env.add-section-variable instead
[elpi.add-const-for-axiom-or-sectionvar,deprecated]
File "./theories/measure.v", line 160, characters 0-40:
Warning: elpi: Using coq.env.add-const for declaring axioms or section
variables is deprecated. Use coq.env.add-axiom or
coq.env.add-section-variable instead
[elpi.add-const-for-axiom-or-sectionvar,deprecated]
File "./theories/measure.v", line 160, characters 0-40:
Warning: elpi: Using coq.env.add-const for declaring axioms or section
variables is deprecated. Use coq.env.add-axiom or
coq.env.add-section-variable instead
[elpi.add-const-for-axiom-or-sectionvar,deprecated]
File "./theories/measure.v", line 172, characters 0-29:
Warning:
The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead
[lib,elpi]
File "./theories/measure.v", line 180, characters 0-29:
Warning:
The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead
[lib,elpi]
File "./theories/measure.v", line 212, characters 6-17:
Error: measurableT already exists.
```

Yeah it's version 0.3.6 on Nixpkgs instead of 0.3.9

Are there limitations on what kinds of inheritance hierarchies that can be formulated in HB?

We are aware of that, and MC analysis dev as well.

What do you mean exactly?

There are some hierarchies which are broken by design, see https://github.com/math-comp/hierarchy-builder/wiki , and HB complains about them

I guess when creating structures that are joins, to quote from MCB,

If a new structure S extends structures that are further apart in the hierarchy more than one such additional link may be needed: precisely one for each pair of structures whose join is S. For example, unitRingType requires three such links, while finFieldType in library finalg requires 11. It is highly advisable to map out the hierarchy when simultaneously extending multiple structures.

So it sounds tedious to join increasingly distinct structures

MC was ported to HB, but not released yet

We could generate automatically join-structures. Currently we don't. But all the nasty machinery to make a join work is done for you. [the main problem is that we would pick a silly name, and at the same time doing the join is typically one line]

This is related to the third entry in the wiki

I have a variation of the same issue again, this time annotating the types or augmenting the constraints of `IsComMonoid`

doesn't seem to help

```
From HB Require Import structures.
From Coq Require Import ssreflect.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of IsSemigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
Fail HB.mixin Record IsComMonoid A of IsMonoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
```

I think this is an instance of https://github.com/math-comp/hierarchy-builder/issues/258

Oh, did you try to write `Monoid A`

already?

Ah, this works

```
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
```

but I'm not sure what the difference is now between `IsMonoid A`

and `Monoid A`

Now I can define the hierarchy but the proof doesn't go through.

```
From HB Require Import structures.
From Coq Require Import ssreflect.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of Semigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
HB.structure Definition ComMonoid := { A of IsComMonoid A }.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Print Module Group.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of Group A & ComMonoid A := { }.
HB.structure Definition ComGroup := { A of IsComGroup A }.
Lemma example (G : ComGroup.type) (a b : G) : (- b + (b + a)) + (- a) = 0.
Proof. rewrite addrC (addrA (opp b)) addNr add0r addNr. Qed.
```

`IsMonoid`

is just a piece of interface, a mixin. `Monoid.type`

is a structure and `Monoid`

is its class, which the set of mixins (transitively closed) which compose the interface of the structure. So `Monoid = IsMonoid + IsSemigroup`

The proof works, there is only one goal left which is `0 = 0`

. You can prefix the line with `by`

which will close it. Did you copy this line from somewhere? It is probably a typo.

I wrote it myself, and if it went through, `by`

would close indeed but one of the rewrites fails:

```
Error: The LHS of addNr
(- _ + _)
does not match any subterm of the goal
```

HB 1.1.0

Hum, it works here (I'm on HB master, but it should make no difference). :-/

Hm, strange. I will override the Nixpkgs version and see

I can replicate this on master

Here is the file, for completeness:

```
From HB Require Import structures.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of Semigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
HB.structure Definition ComMonoid := { A of IsComMonoid A }.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Print Module Group.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of Group A & ComMonoid A := { }.
HB.structure Definition ComGroup := { A of IsComGroup A }.
Lemma example (G : ComGroup.type) (a b : G) : (- b + (b + a)) + (- a) = 0.
Proof. Fail rewrite addrC, (addrA (opp b)), addNr, add0r, addNr. Admitted.
```

I've to rush now, but it seems you are using Coq's vanilla rewrite, which is picky about implicit arguments (sometimes you have to unfold things your don't see). If you use the ssreflect one, does it still fail?

It fails using ssreflect's rewrite and Coq's rewrite.

For me it works with ssreflect (and indeed not with vanilla Coq)

```
Require Import ssreflect ssrfun ssrbool.
From HB Require Import structures.
HB.mixin Record IsSemigroup A := {
add : A -> A -> A;
addrA : forall (x y z : A), add x (add y z) = add (add x y) z;
}.
HB.structure Definition Semigroup := { A of IsSemigroup A }.
Infix "+" := add.
HB.mixin Record IsMonoid A of Semigroup A := {
zero : A;
add0r : forall (x : A), zero + x = x;
}.
HB.structure Definition Monoid := { A of IsMonoid A }.
Notation "0" := zero.
HB.mixin Record IsComMonoid A of Monoid A := {
addrC : forall (x y : A), x + y = y + x;
}.
HB.structure Definition ComMonoid := { A of IsComMonoid A }.
HB.mixin Record IsGroup A of Monoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition Group := { A of IsGroup A }.
Print Module Group.
Notation "- x" := (opp x).
HB.mixin Record IsComGroup A of Group A & ComMonoid A := { }.
HB.structure Definition ComGroup := { A of IsComGroup A }.
Lemma example (G : ComGroup.type) (a b : G) : (- b + (b + a)) + (- a) = 0.
Proof. by rewrite addrC (addrA (opp b)) addNr add0r addNr. Qed.
```

Last updated: Oct 13 2024 at 01:02 UTC