The norm of a normedModule should be valued in a realType, not in its field of scalar. Definition of subNumDomain.

[mkerjean]

Consider V : normedModType K with K : numFieldType. As of now, its norm is of type `| _ | : V -> K. However, it should be more specifically of type `| _ | : V -> R for R: realTypeand a subType of K. In particular, this will become handy in complex analysis, or allow more generality in the Hahn-Banach theorem, which, as of now, can be instantiated only on normed modules over R.

An easy way to do that is to change the definition of normedModule as such:

HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule (C: numDomainType)
  (R : realType) V   
& PseudoMetricNormedZmod R V & ConvexTvs C V := {
  val : R -> C ;
  ival : injective val;  
  normrZ : forall (l : C) (x : V), val (`| l *: x |) = `| l | * (val `| x |) :> C
}.

However, this is a bit pedestrian as it overlooks the availability of subtypes to handle R. Sadly, the definition of subNumDomain seems to be intricate, due to duplication issues between the domain and a codomain of a norm.

Looking at the definition of NumDomain,

 #[short(type="numDomainType")]
HB.structure Definition NumDomain := { R of
     GRing.IntegralDomain R &
     NumZmodule R &
     NormedZmodule (POrderZmodule.clone R _) R &
     NumZmod_isNumRing R
  }. 

the definition of SubNumDomain should be

 #[short(type="subNumDomainType")]
HB.structure Definition SubNumDomain (M : numDomainType) (S : pred M) := 
{ U of
    SubChoice S U &
     GRing.IntegralDomain U &
     NumZmodule U &
     SubNormedZmodule (POrderZmodule.clone U _) M S U &
     NumZmod_isNumRing U
  }.

However, this triggers an error, as M is supposed to be a numDomain over M, not U. Likewise

#[short(type="subNumDomainType")]
HB.structure Definition SubNumDomain (M : numDomainType) (S : pred M) := 
{ U of
    SubChoice S U &
     GRing.IntegralDomain U &
     NumZmodule U &
     SubNormedZmodule (POrderZmodule.clone M _) M S U &
     NumZmod_isNumRing U
  }.

triggers an error, as U is supposed to be a numDomain over U, not M.

How can we solve that ? It looks like this approach of using subtypes does not work. Could this be an issue of making hierarchy-builder understand the \val : U -> M coercion between norm : U -> U and norm : M -> M when declaring the subNumDomainType structure?

@CohenCyril, maybe you have some HB magic in mind that could help us ?

[mkerjean]

I tried to change the subNormedZmodType structure by adding a coval parameter, but this does not work either, as rocq does not find the right type on val when defining subNumDomainType.

HB.mixin Record Zmodule_isSubNormed (R : porderZmodType)  (R' : porderZmodType) (coval :  R' -> R) (M : normedZmodType R)
  (S : pred M) U & SubType M S U & NormedZmodule R' U := {
  norm_valE : forall x : U, norm ((val : U -> M) x) = coval (norm x)
}.

#[short(type="subNormedZmodType")]
HB.structure Definition SubNormedZmodule (R : porderZmodType) (R' : porderZmodType) (coval :  R' -> R) 
    (M : normedZmodType R) (S : pred M) :=
  { U of SubChoice M S U & Num.NormedZmodule R U & GRing.SubZmodule M S U
       & @Zmodule_isSubNormed R R' coval M S U }.

[...]

#[short(type="subNumDomainType")]
  HB.structure Definition SubNumDomain (M : numDomainType) (S : pred M) :=
  { U of
      SubChoice M S U &  NumDomain U &
      @SubNormedZmodule (POrderZmodule.clone U _) (POrderZmodule.clone M _)  (\val) M S U
  }.