Deprecating Mathlib/Data/Analysis

Stream: mathlib4

[Anne Baanen]

The files Mathlib/Data/Analysis/Filter.lean and Mathlib/Data/Analysis/Topology.lean re-implement a bit of the theory of filters and of topology from 2017. The files are experimental, and they have received no real features or usage since they were first made. Sounds like they are clearly ready for deprecation. Any project that wants to adopt these modules, or shall I deprecate them without replacement?

(I came across this while tracking down the directories imported by Mathlib/Data. Analysis and topology are only imported by Data/Real, Data/Complex and Data/Analysis.)

[Jireh Loreaux]

@Mario Carneiro do you want to explain a bit about the intended purpose of these files?

[Mario Carneiro]

they provide a computational interpretation of filters, continuous functions etc, by associating elements of a type with a subbase operation

[Mario Carneiro]

for example you can do this for the topology of the reals by using rational intervals

[Mario Carneiro]

I also want to remark that I don't think the described deprecation flowchart is right (speaking more generally than this specific material). Just because a theorem isn't getting use doesn't mean it should be deleted. Unless you mean deprecation as in people should avoid it, but who is that going to affect in the first place if it's not being used? It's not even an argument that it shouldn't be used, only that as a matter of fact it is not, which is at best weak evidence that it is not a good API.

[Wrenna Robson]

That feels right to me, certainly - if there's a general use at least.

[Mario Carneiro]

sorry, I don't know who you are agreeing with

[Wrenna Robson]

Sorry: you.

[Wrenna Robson]

For an example of a file I myself created, I think Mathlib.Topology.MetricSpace.Infsep is missing something of a use right now, but it is intended to provide the analysis way of spelling "minimum distance of a set", essentially: I think it is worth keeping, and the API was based off of Set.diam and I think is pretty sensible. But, well, ultimately I could see a deprecation argument. I think this would be somewhat overzealous though - and even more so in the case of the files you mention!

[Mario Carneiro]

To be honest I never really expected those files to get much use, but the reason for this is that I don't think it's an area that is very well studied. You need to care about both topology and computation (in the Brouwer sense) at the same time to be lead to this approach

[Mario Carneiro]

I think it's related to realizability models, it's not an area I know much about

[Jireh Loreaux]

Mario Carneiro said:

they provide a computational interpretation of filters, continuous functions etc, by associating elements of a type with a subbase operation

Sure, I did actually read the module documentation :wink:. I guess my question could have been more specific: what abilities does this computational interpretation unlock? Was the goal to use it in a tactic at some point?

[Mario Carneiro]

No, it wasn't for a tactic. It was actually computation for its own sake when I wrote it. You should be able to use it in some #eval things but it's still a bit high order so it's hard to see exactly what you would be doing

[Mario Carneiro]

there are some things where you can for example reduce checking that a function is continuous to a countable sequence of decidable tests

[Mario Carneiro]

if you have an open set, and provide a point in it, you can compute a specific interval that is in the set

[Mario Carneiro]

this is kind of like the representation of a topology you might find in sage

[Violeta Hernández]

Ah, the age old "should Mathlib care about computation" question.

[Violeta Hernández]

Independently of this, I really wish we had an answer one way or the other.

[Anne Baanen]

What I don't understand then is: the files claim to be experimental. I thought this meant: the experiment is to see if they are more useful than the current implementations. If they have not seen use since 2017, then they are not more useful. So we should stop spending our effort on maintaining these files (which has probably been more effort than writing them in the first place), and mark them as deprecated.

[Anne Baanen]

Violeta Hernández said:

Independently of this, I really wish we had an answer one way or the other.

When I joined the Mathlib community in 2019 I was told directly that Mathlib does not care about computation. Did we change our mind?

(Which would be great for me, since I am an intuitionist!)

[Wrenna Robson]

I certainly care about computation.

[Violeta Hernández]

So we should stop spending our effort on maintaining these files (which has probably been more effort than writing them in the first place), and mark them as deprecated.

As someone who has had to painstakingly fix other files that haven't been used since 2017, I'd really like to stress this point.