PseudoMetricSpace.toUniformSpace

Stream: mathlib4

[Matthew Ballard]

Why is toUniformSpace a field of docs#PseudoMetricSpace instead having PseudoMetricSpace extend UniformSpace?

[Jireh Loreaux]

(deleted)

[Matthew Ballard]

Related question: how can I make the following work

import Mathlib.Topology.MetricSpace.PseudoMetric

variable (M₁ M₃ : Type*) [PseudoMetricSpace M₁] [PseudoMetricSpace M₃]

example :
    (instTopologicalSpaceProd : TopologicalSpace (M₁ × M₃)) = PseudoMetricSpace.toUniformSpace.toTopologicalSpace := by
  with_reducible_and_instances rfl -- fails

[Matthew Ballard]

It doesn’t want to unfold PseudoMetricSpace.toUniformSpace

[Yury G. Kudryashov]

What if you use extends instead of an explicit field?

[Yury G. Kudryashov]

It's possible that someone chose an explicit field for some reason that no longer applies in Lean 4.

[Matthew Ballard]

At first glance, I get many errors

[Yury G. Kudryashov]

I wonder why

[Matthew Ballard]

Looks like most come from the autoparams from the other fields. Just sorry-ing everything removes errors until the docs#Prod.pseudoMetricSpaceMax but still not unfolding.

[Jireh Loreaux]

I think the issue is that you want it for the default by intros; rfl proof of uniformity_dist.

[Matthew Ballard]

That was the source of most errors when moving to a parent class

[Jireh Loreaux]

And for that to work in general you need the special construction docs#UniformSpace.ofDist to be supplied as the default field.

[Jireh Loreaux]

This is all coming back to me now from when I added bornology.

[Yury G. Kudryashov]

But many constructions already have a UniformSpace instance.

[Yury G. Kudryashov]

In fact, I think that forcing a user to explicitly provide toUniformSpace if there is no instance yet is a good thing.

[Matthew Ballard]

I was looking at the wrong place. I need to make docs#PseudoEMetricSpace.toPseudoMetricSpaceOfDist reducible

[Matthew Ballard]

It was choking there in the definition of docs#Prod.pseudoMetricSpaceMax

[Jireh Loreaux]

Yury, I can see why we might want to always (or mostly) provide our own UniformSpace instance in Mathlib, but for downstream users I think it's quite inconvenient if things like this are not autoparams.

[Eric Wieser]

I think we need a tryThisParam instead of autoParam that inserts a template for the user, so that they are at least aware that a default is being use

[Matthew Ballard]

You have to guess what the autoParam is trying to do when it errors right now which is extra overhead