emetric --> pseudo_emetric

Stream: general

[Riccardo Brasca]

In #7672 Sébastien found some uses of [emetric_space] that can be weakened to [pseudo_emetric_space], without touching the proof. I guess there are more, and similarly for [metric_space], [normed_group], [normed_space] (we recently introduce these classes because we needed them for LTE).

Is it possible to automatize this process? There are just 38 [emetric_space... and 91 [emetric_space..., with some time can also be done by hand.

I have no idea if this is very hard or not, but ideally one should check every lemma that has a [emetric_space, but not explicitly written (because it appears before as variable [emetric_space...)

[Scott Morrison]

One problem is just that we'd have to run the tool multiple times, as each time we relax a hypothesis new lemmas may become "relaxable". I doubt it's worth automating this process, which would be much harder.

[Scott Morrison]

I wouldn't mind having this tool available for other things: e.g. I have several open PRs just consisting of relaxing comm_ring to ring or field to division_ring when it's possible to do so without touching the proof.

[Riccardo Brasca]

Ah, good point!

[Alex J. Best]

The generalization linter I spoke about at lean together 2021 aims to do exactly this (https://www.youtube.com/watch?v=4W-B8tGJUME&ab_channel=leanprovercommunity). It mostly works and I'm working on improving it currently. The main problem right now is just that it is a little slow, which makes it difficult to use interactively in big files (i.e. it times out). This makes using it iteratively a pain, as Scott points out this is really the way you want to use it.
For example running it on src/topology/metric_space/basic.lean it currently outputs

$ lean src/topology/metric_space/basic.lean
/- Checking 310 declarations (plus 206 automatically generated ones) in the current file -/

/- The `generalisation_linter` linter reports: -/
/- typeclass generalisations may be possible: -/
#print metric.ball /- _inst_1: pseudo_metric_space ↝ has_dist
 -/
#print metric.closed_ball /- _inst_1: pseudo_metric_space ↝ has_dist
 -/
#print metric.sphere /- _inst_1: pseudo_metric_space ↝ has_dist
 -/
#print metric.complete_of_cauchy_seq_tendsto /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space
 -/
#print totally_bounded_Icc /- _inst_1: pseudo_metric_space ↝ uniform_space
 -/
#print metric.bounded /- _inst_1: pseudo_metric_space ↝ has_dist
 -/
#print metric.diam /- _inst_1: pseudo_metric_space ↝ pseudo_emetric_space
 -/
#print metric.uniform_embedding_iff' /- _inst_3: metric_space ↝ pseudo_metric_space
 -/
#print exists_subset_Union_ball_radius_lt /- _inst_2: metric_space ↝ normal_space pseudo_metric_space
 -/
#print exists_subset_Union_ball_radius_pos_lt /- _inst_2: metric_space ↝ normal_space pseudo_metric_space
 -/
#print metric.second_countable_of_countable_discretization /- _inst_3: metric_space ↝ proper_space pseudo_metric_space
 -/

This takes a few minutes at present which is annoying.
Note that some of these are defs which you may or may not want to generalize, and that generalizations like metric_space ↝ normal_space pseudo_metric_space look mathematically trivial to me.

[Scott Morrison]

Thanks, nice talk! I missed most of LT21, timezones. :-(

Could we have this sooner rather than later even if it is slow? I would use it already.

[Scott Morrison]

Often I know exactly which generalization I'm looking for (e.g. I want to find all the places I can relax [field] to [division_ring].). Presumably your linter could be much faster if it only had to test for one particular possibility. (It's certainly good to have the universal one as well.)

[Alex J. Best]

Scott Morrison said:

Often I know exactly which generalization I'm looking for (e.g. I want to find all the places I can relax [field] to [division_ring].). Presumably your linter could be much faster if it only had to test for one particular possibility. (It's certainly good to have the universal one as well.)

Thanks, that's a nice idea, it'll definitely cut the time down a bit and make this more usable, though with the way it currently works I think it'd still have to build the whole TC graph as the first step. What I really need is a way to cache that step between runs also.

[Alex J. Best]

Scott Morrison said:

Could we have this sooner rather than later even if it is slow? I would use it already.

Noted :smile:

[Scott Morrison]

(Of course, I don't mean to pressure you; just that I don't mind it being slow!)

[Yaël Dillies]

In general, can't we decide to run some linters every now and then rather than in CI? This linter has a bit of a one-time job. We don't need it to run that many times over each declarations.

[Yaël Dillies]

Or maybe we want to, because then the people who created the problem noticed by the linter will see it and can better correct it than someone else?

[Scott Morrison]

I don't think this one should ever be run in CI. There are many good reasons not to state the most general possible theorems.

[Scott Morrison]

I think the plan is only that it is a linter you run by hand.

[Yaël Dillies]

Yeah okay, that's what I would deem reasonable.

[Riccardo Brasca]

That's great! I also don't mind using one or two cores of my university mainframe to test this (nobody uses it...)