New fields in MetricSpace

Stream: mathlib4

[Bjørn Kjos-Hanssen]

I made a metric_space in Lean 3, and want to convert it to Lean 4. However, it seems that MetricSpace has a whole host of new fields like edist_dist and Bornology. Is there a version of metric spaces in Lean 4 without all these add-ons?

[Yury G. Kudryashov]

Both were added in Lean 3.

[Yury G. Kudryashov]

For edist_dist, we had a tactic to fill it in.

[Yury G. Kudryashov]

I removed it while porting (because my Lean 4 metaprogramming skills are between very low and non-existent).

[Notification Bot]

This topic was moved here from #lean4 > New fields in MetricSpace by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Bjørn Kjos-Hanssen I moved the topic to a more appropriate stream.

[Yury G. Kudryashov]

MetricSpace should be able to fill in Bornology-related fields automatically (possibly, after you fill in edist_dist). If it fails, then this is a bug.

[Yury G. Kudryashov]

And restoring the autoparam for edist_dist is very welcome.

[Bjørn Kjos-Hanssen]

Thanks @Yury G. Kudryashov So basically `[exact (ennreal.of_real_eq_coe_nnreal _).symm ?

[Yury G. Kudryashov]

If you have a code that works, then please make a PR that removes (almost) all the edist_dist fields from instances.

[Yury G. Kudryashov]

It should work for rfl too.

[Bjørn Kjos-Hanssen]

Thanks for the encouragement, actually

        edist_dist         := (λ x y ↦ by exact (ENNReal.ofReal_eq_coe_nnreal _).symm)

seems to do the trick. But I'm not sure how to turn that into a PR.

[Bjørn Kjos-Hanssen]

And you're right, only edist_dist needs to be supplied.

[Scott Morrison]

@Bjørn Kjos-Hanssen, is https://leanprover-community.github.io/contribute/index.html what you are looking for? If you need some more specific advice on making a PR, please ask.

[Yury G. Kudryashov]

It looks like @Adam Topaz already answered my question about tactic here

[Yury G. Kudryashov]

You can try to add this definition and add := by edist_dist_tac to the edist_dist field.

[Yury G. Kudryashov]

Or I can try to do it tomorrow.

[Bjørn Kjos-Hanssen]

I see it says #noalign pseudo_metric_space.edist_dist_tac is that the part to change?

[Scott Morrison]

You can just delete that #noalign, there's no point writing #align or #noalign statement for metaprogamming code.