Stream: math-comp users

Topic: Building a comUnitRingType with Hierarchy Builder

view this post on Zulip Florent Hivert (Nov 22 2023 at 21:31):

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 !

view this post on Zulip Pierre Roux (Nov 22 2023 at 21:52):

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?

view this post on Zulip Pierre Roux (Nov 22 2023 at 21:53):

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

view this post on Zulip Florent Hivert (Nov 22 2023 at 22:07):

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 ?

view this post on Zulip Pierre Roux (Nov 23 2023 at 06:56):

Yes, that's certainly the explanation.

view this post on Zulip Cyril Cohen (Nov 23 2023 at 08:28):

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":

view this post on Zulip Florent Hivert (Nov 23 2023 at 08:33):

Excellent !

Last updated: Oct 13 2024 at 01:02 UTC