Generalised notion of (Pseudo)MetricSpace

Stream: general

[Edward van de Meent]

I'm currently in the process of defining a generalised notion of Metric, such that the codomain is less constricted. with the current definition, the only options (as far as i know) are to either use Real, NNReal, or ENNReal. however, for my project i need to be able to use Nat (or ENat, i'm not quite sure about that yet). i have already made definitions for GDist, GPseudoMetricSpace, and GMetricSpace. I would like some help and/or advice about how to go about porting lemmas and theorems about these spaces.
My definition extends these notions to mostly only require an instance LinearOrderedCancelAddCommMonoid β, which all of the current possible versions should support i think? (maybe not Real, but im not too sure that this should be a problem, as for most notions of distance that i'm aware of, you cannot have negative distances.)
About 400 lines into copying and rewriting lemmas of PseudoMetricSpace i realised that there quite possibly is a better way of going about this kind of porting... As i'm new to this community, i'm not quite sure how to contribute, or how the process of generalising definitions goes...

Can someone explain how i should go about getting this notion into mathlib, and are there people willing to help with such a process?

I currently have my definitions and ported lemmas at the repo for the project i'm currently working on in the folders GPseudoMetricSpace and GMetricSpace, but i understand if it will be better for workflow if this gets moved somewhere else

[Sébastien Gouëzel]

I would strongly advise against adding another typeclass with data, since it is not really necessary as your spaces are in fact particular cases of metric spaces (or emetric spaces): instead, you could have a mixin like IsNatValuedDist, saying that the distance is Nat-valued on a metric space. On a space satisfying [PseudoMetricSpace X] [IsNatValuedDist X], you could introduce a new function natDist (which would just be the cast of the distance function to Nat) and prove the properties you need on it. With this approach, you wouldn't have to reprove all the topological properties of the metric spaces, and focus on the novelties that the Nat-valued distance would give you.

[Edward van de Meent]

i suppose that would indeed work for my case... however, you'd have to have such a mixin for each codomain, and that seems to me like the less elegant way of going about this, rather than just having a class GDist α β where the type is a parameter

[Edward van de Meent]

it would be like defining only the symmetric groups, along with mixins saying "only look at these elements today"

[Edward van de Meent]

rather than the general notion of a group

[Sébastien Gouëzel]

The problem with the GDist approach is that the way the real, nnreal and ennreal distances are mixed together is highly nontrivial in mathlib (notably to make sure that the uniform structure coming from the three of them is definitionally the same, which is crucial for many things), so having just one class and three independent implementations for real, nnreal and ennreal would just not work. The current implementation is one of mathlib's most delicate constructions, that's why I would just build on top of it instead of trying to tinker with it.

[Edward van de Meent]

i think there is a single property which all three of those have, which lets you define that structure, right? then maybe we would rather have a singular definition for that uniform structure such that it works... i don't see the problem with this approach yet

[Edward van de Meent]

i looked a bit, and for domain Real the property that was used was that ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε...

[Edward van de Meent]

looks to me like the same was used for ENNReal

[Edward van de Meent]

this can just be an extra assumption before defining the induced UniformSpace

[Sébastien Gouëzel]

If you look at the definition of metric spaces and emetric spaces in mathlib, you will see that they are not symmetric: a metric space contains an emetric space as a subfield (for good reasons related to forgetful inheritance, as I was trying to explain above). This means that you can not have a single class that will work for everything.

[Edward van de Meent]

so then other than the fact that the domain allows for infinity, what's the difference?

[Edward van de Meent]

at the very least the pseudometric and pseudoEMetric versions don't look to be dependent on each other...

[Sébastien Gouëzel]

From the mathematical point of view, the only difference is that the distance is allowed to take the value infinity. From the implementation point of view, there are subtle details because when you want to look at the topological structure on a metric space, typeclass inference could follow different pathes, going or not through the emetric structure, and you want the topological structure along the different paths to be definitionally equal.

[Sébastien Gouëzel]

Edward van de Meent said:

at the very least the pseudometric and pseudoEMetric versions don't look to be dependent on each other...

You can have a look at the definition of a pseudometric space: there are both dist and edist fields there, for the reason I have just explained. While there is no dist field in the definition of pseudoemetric spaces. The definitions are really different.

[Eric Wieser]

Would there be any problem in having GPseudoMetricSpace extend PseudoMetricSpace, along with a field stating they agree?

[Edward van de Meent]

the whole point is having it be the other way around though?

[Eric Wieser]

The advantage over IsNatValuedDist is that you could potentially have a computable distance function

[Edward van de Meent]

because you'd like to say that a metric space really is just the special case where the domain is Real

[Edward van de Meent]

i can imagine having something like

abbrev MetricSpace (α : Type u) := GMetricSpace α ℝ

[Edward van de Meent]

although i'm can imagine it's not quite going to be that easy...

[Jireh Loreaux]

You're missing the (tricky and subtle) point that Sébastien Gouëzel is making about forgetful inheritance. If you do something like this, then all of a sudden you will break things, because there will be multiple topological structures that are not definitionally equal.

[Eric Wieser]

Edward van de Meent said:

the whole point is having it be the other way around though?

Oh indeed, I'm just explaining how you could build something on top of what mathlib has if a refactor turns out to be too much work.

[Edward van de Meent]

Jireh Loreaux said:

You're missing the (tricky and subtle) point that Sébastien Gouëzel is making about forgetful inheritance. If you do something like this, then all of a sudden you will break things, because there will be multiple topological structures that are not definitionally equal.

if you make sure that the ordering on the restriction from ENNReal to NNReal is definitionally equivalent, i think that should fix it?

[Eric Wieser]

It's not clear to me how the epsilon/delta argument in docs#UniformSpace.ofDist would generalize to Nat

[Edward van de Meent]

there is no natural instance of UniformSpace on GMetricSpace i think... because you don't get to split distances per sé

[Eric Wieser]

Right, and therein lies the issue; you now need a separate typeclass that says "the uniform space and metric space agree", which is a much larger (but not impossible) refactor

[Eric Wieser]

Now, maybe you can get away with something along the lines of

• Introduce GMetricSpace α ℝ
• Introduce IsInducedUniformity α ℝ
• Redefine MetricSpace as the combination of the above two classes

[Jireh Loreaux]

Others have needed Nat-valued metrics before. I think the simplest thing is to add a mixin class for that, with some simple API. If we end up needing more than just Nat, then we consider a larger refactor.

[Eric Wieser]

One refactor that I think would be sensible would be to combine the EDist, NNDist, and Dist classes into a single class, and restore edist, nndist, and dist as abbreviations

[Edward van de Meent]

just so i get this...
if you define something like

toUniformSpace (...) (hb:∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε) : UniformSpace α := ....

what goes wrong?

[Jireh Loreaux]

Also note, Edward, that ENNReal isn't cancellative, so it doesn't fit your current type class constraints (likely this is minor).

[Edward van de Meent]

ah, good catch

[Jireh Loreaux]

See the relevant chapter of #mil for why it breaks things.

[Jireh Loreaux]

(I'll try to find it, but I'm on mobile)

[Edward van de Meent]

i'm guessing it's in the chapter about metric spaces?

[Jireh Loreaux]

Maybe I'm thinking of the wrong reference, sorry

[Yury G. Kudryashov]

You can add

class NatDist (X : Type*) where
  natDist : X -> X -> Nat

class NatMetricSpace extends MetricSpace X, NatDist X where
  dist_eq : ∀ x y, dist x y = natDist x y

def NatMetricSpace.ofNatDist [NatDist X] (hsymm : ∀ x y : X, natDist x y = natDist y x)
    (htriangle : ∀ x y z : X, natDist x z ≤ natDist x y + natDist y z) :
    NatMetricSpace X where
  -- fill in all elements, probably using discrete uniformity

[Yury G. Kudryashov]

Generalizing all *Dist will make it hard to extend both Dist and EDIst in a single typeclass.