Stream: math-comp users

Topic: Missing join of NormedZmodule and POrderZmodule

Li Zhou (Feb 26 2024 at 18:12):

In mathcomp/algebra/ssrnum.v, there is no join of NormedZmodule and POrderZmodule. The structure inherits from both is numDomainType, which adds isNumRing properties.
This makes defining any types that inherits from NormedZmodule and POrder but lacking isNumRing impossible. For example:

#[short(type="porderNormedLModType")]
HB.structure Definition porderNormedLModule (R : numDomainType) := { T of
    GRing.Lmodule R T &
    Num.POrderedZmodule T &
    Num.NormedZmodule R T
  }.

fails with message
`Error: You must declare the hierarchy bottom-up or addd a missing join. There are two ways out:

• declare structure porderNormedLModule before structure Num.NumDomain if Num.NumDomain inherits from it;
• declare an additional structure that inherits from both Num.NormedZmodule and POrder and from which porderNormedLModule and/or Num.NumDomain inherit.`

Both suggestions fail unless some changes are made to ssrnum.v before declaring numDomainType.
More specifically, we formalized some theories of ordered topological vector space (inherits from both Porder and normedZmodule, but not a numDomainType), and we faced this problem when we updated from mathcomp.1.9.0 to 2.2.0.

Any suggestions to solve the problem? In particular, is there a third suggestion that doesn't need to modify mathcomp?

Last updated: Oct 13 2024 at 01:02 UTC