I'm learning how to use HB, and I don't understand how to build instance whose axioms are just union of already known instance.

I'm trying to build a `comUnitRingType`

using HB. I currently managed to have unit ring, commutative ring and commutative algebra, that is the following commands succeed

```
Check ([unitRingType of {tfps R n}]). (* assume that R is a unitRingType *)
Check ([comRingType of {tfps R n}]). (* assume that R is a comRingType *)
```

But

```
Check ([comUnitRingType of {tfps R n}]).
```

fails

```
The term "id_phant" has type "phantom Type {tfps R n} -> phantom Type {tfps R n}"
while it is expected to have type "unify Type Type {tfps R n} ?cT nomsg".
```

I can't find the command to declare the instance...

I managed to have commutative algebra with

```
HB.instance Definition _ :=
GRing.Lalgebra_isComAlgebra.Build _ {tfps R n}.
```

I can't find the equivalent, and it look suspicious to me that I didn't pass any axiom in the previous command.

Thanks for any help !

Strange, I would have expected whichever of unitRing/comRing is built last to build the comUnitRing, maybe try `HB.instance Definition _ := ComRing.on {tfps R n}`

to try rebuild it?

As a side note, you no longer need the square bracket notations, `Check {tfps R n} : comRingType`

should now work.

Thanks for the tip. It seems to solve the problem. Maybe this is due to the fact that in the section where I defined the comRingType instance, R was just a comRingType, and similarly for unitRingType. So until now It didn't had the possibility to have a comUnitRingType instance.

Does that makes sense ?

Yes, that's certainly the explanation.

Florent Hivert said:

Thanks for the tip. It seems to solve the problem. Maybe this is due to the fact that in the section where I defined the comRingType instance, R was just a comRingType, and similarly for unitRingType. So until now It didn't had the possibility to have a comUnitRingType instance.

Does that makes sense ?

It makes sense, and there is an ongoing work to solve that issue under the codename "saturation":

- https://github.com/math-comp/hierarchy-builder/issues/337
- https://github.com/math-comp/hierarchy-builder/issues/338

Excellent !

Last updated: Jul 25 2024 at 15:02 UTC