Topological structures on numFields

[affeldt-aist]

Is this change of canonical structures correct?

[CohenCyril]

Is this change of canonical structures correct?

nop, there should be a structure merge between numDomainType and pointedType

[CohenCyril]

there should be a "pointedNumDomain" Structure :-/
But it's too heavy with HB...

[affeldt-aist]

But it's too heavy with HB...

You mean without?

[CohenCyril]

But it's too heavy with HB...

You mean without?

yes, without

[CohenCyril]

So in the end, with @mkerjean suggestion, this will happen... but as part of a bigger commit making all numFieldType canonically normedModType
(EDIT: replaced numDomainType by numFieldType)

[affeldt-aist]

there should be a "pointedNumDomain" Structure :-/
But it's too heavy with HB...

Something like that?

Module PointedNumDomain.
Section ClassDef.
Record class_of T := Class {
  base : Num.NumDomain.class_of T ;
  pointed_mixin : Pointed.point_of T }.
Local Coercion base : class_of >-> Num.NumDomain.class_of.
Local Coercion pointed_base T (class_of_T : class_of T) :=
  @Pointed.Class _ class_of_T (pointed_mixin class_of_T).

Structure type := Pack { sort ; _ : class_of sort }.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack T c.
Definition pack (b0 : Num.NumDomain.class_of T) (pm0 : @Pointed.point_of T) :=
  fun bT (b : Num.NumDomain.class_of T)
    & phant_id (@Num.NumDomain.class bT) b =>
  fun pm & phant_id pm0 pm => @Pack T (@Class T b pm).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition ringType := @GRing.Ring.Pack cT xclass.
Definition comRingType := @GRing.ComRing.Pack cT xclass.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
Definition numDomainType := @Num.NumDomain.Pack cT xclass.
Definition pointedType := @Pointed.Pack cT xclass.
End ClassDef.

Module Exports.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion base  : class_of >-> Num.NumDomain.class_of.
Coercion pointed_base : class_of >-> Pointed.class_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> Num.NumDomain.type.
Canonical numDomainType.
Coercion pointedType : type >-> Pointed.type.
Canonical pointedType.
Notation pointedNumDomainType := type.
Notation PointedNumDomainType T m := (@pack T m _ id _ id _).
Notation "[ 'pointedNumDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'pointedNumDomainType'  'of'  T  'for'  cT ]") : form_scope.
Notation "[ 'pointedNumDomainType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'pointedNumDomainType'  'of'  T ]") : form_scope.
End Exports.
End PointedNumDomain.
Import PointedNumDomain.Exports.

[CohenCyril]

Hum, no, I meant, with @mkerjean's suggestion, we do not have dedicated structures, but we indeed do what your PR originally did, but on a larger scale (every structure above num field should have coercions and canonicals to pointed, filtered, topological, pseudometric and normed types...)
(EDIT: I replaced num domain by num field)

[mkerjean]

Hum, no, I meant, with @mkerjean's suggestion, we do not have dedicated structures, but we indeed do what your PR originally did, but on a larger scale (every structure above num domains should have coercions and canonicals to pointed, filtered, topological, pseudometric and normed types...)

I'll be updating this PR today (AoE maybe).

[affeldt-aist]

(to be closed, see #205)

[CohenCyril]

Subsumed by #205