Importing Data.String.Basic

Stream: mathlib4

[Chris Hughes]

Data.String.Basic is pretty difficult to port right now. The main dependency on this file is a has_repr for multisets which uses the definition of le as well as some difficult to prove properties of le to show the repr is well defined on the quotient. There are some other reprs that depend on this as well. There are three solutions to this. We could move le to Data.String.Defs and make the repr instane a meta instance, we could move the reprs to seperate files or we could wait until Data.String.Basic is ported before porting Data.Multiset.Sort.

/poll What should we do?
Move has_repr instance into seperate files
Move le into string.defs and make the instances meta
Port Data.String.Basic before doing anything else
Something else

[Arien Malec]

Isn't this in the category of "everything interesting wants to be in Std anyway"?

[Chris Hughes]

I think definitions about strings are of interest to a lot of people and theorems about strings are of interest to almost no-one.

[Arien Malec]

I think proving core APIs are correct is good for API consumers generally but not for mathlib outside of, dunno, FSA etc.

[Eric Wieser]

Polls have to be all by themselves in a post

[Henrik Böving]

Chris Hughes said:

I think definitions about strings are of interest to a lot of people and theorems about strings are of interest to almost no-one.

I mean if we eventually end up writing parser libraries or something with formal guarantees theorems of strings could end up being very interesting I guess.

[Heather Macbeth]

I think we should take Chris' first option: move multiset.has_repr out of data.multiset.sort into a new file data.multiset.string (or similar). There's no need to block the mathematical development of multisets on the theory of strings.

[Eric Wieser]

Can we do something even easier, which is just comment out the declaration with a porting comment?

[Eric Wieser]

One other thing to note; the current has_repr instance is actually pretty stupid:

import data.multiset.sort

#eval ({1, 2, 11, 12} : multiset nat) -- {1, 11, 12, 2}

I would claim that no one wants to see the elements in that order

[Chris Hughes]

It mucks up the output of Port status if we don't port it.

[Eric Wieser]

How so?

[Eric Wieser]

#port-status is only an approximation; the final pass of "did we really port everything" is going to come from asking mathport to look for unaligned declarations

[Chris Hughes]

Well won't it only show the files that have all of their dependencies on mathlib3 ported, so if we never port Data.String.Basic all of its dependencies won't show unless we change mathlib3.

[Eric Wieser]

Are you sure it cares about transitive dependencies and not direct dependencies?

[Heather Macbeth]

I think it only cares about direct dependencies, we've encountered this before.

[Eric Wieser]

Because if it's the former, there are only two such files to worry about, and you are already aware of the mathematically interesting one

[Chris Hughes]

What are the two sectioms for "all dependencies" and "immediate dependencies" then?

[Eric Wieser]

It sounds like the effect of not porting Data.String.Basic will be that the finiteness files end up in the second heading

[Eric Wieser]

I don't think that's a problem

[Mario Carneiro]

Wait, why is Data.String.Basic being considered for not-porting? Even if everything in it is moved to std or noaligned or whatever, the file itself should still be ported and marked as such even if it's basically empty

[Chris Hughes]

Because it's really hard to prove the theorems

[Chris Hughes]

It's not for not porting, just low priority, and it will be blocking a lot of progress pretty soon.

[Mario Carneiro]

If there are practical definitions that depend on theorems that we aren't interested in proving at the moment (but which we expect to be true), you can work around this by using an opaque to define the function without proving the theorem

[Mario Carneiro]

I think we also need a way to say "this is an ad-hoc port but pretend it is ported anyway for the purpose of later files" to the port-status bot. This is what we already do for files in Tactic.* and lean 3 core files but we might need it for selected files outside those areas as well

[Mario Carneiro]

that way we could just ad-hoc port the file and then update the bot so that later files are unblocked