upstreaming of List/Array material

Stream: batteries

[Kim Morrison]

I'd like to move some more material about basic operations on List and Array from Std/Boost up to the lean4 repository. My initial proposal is:

• Upstream Std/Data/List | Array/Init/Lemmas.lean, which have no prerequisites and are about basic operations.
• Initially don't touch Std/Data/List | Array/Basic.lean, which add many new operations.
• Next, upstream the subset of Std/Data/List | Array/Lemmas.lean which are only in terms of operations already in lean4.
• Later, I would like to upstream the list operations mapIdx / findIdx / indexOf / count (and hence possibly Std/Data/List/Count.lean), and the array operations attach and join, but this would require some review of their API first, and possibly more work to complete it.
• Otherwise, the new definitions and their theorems should stay in Boost, although in future we may want to do a case-by-case review of definitions to promote.

Some of these files have ancient "Authors:" lines that don't accurately reflect later contributions, so I'm happy to take (here or via DM) suggestions for additions. Similarly I'm happy to make additions to CODEOWNERS here.

[Kim Morrison]

lean4#3975 implements the first bullet point above, but I'll wait on merging until people have had time to see the above.

[Mario Carneiro]

One point worth noting is that you can't really 'upstream Std/Data/List/Init/Lemmas.lean' (or it's non init version for that matter), in the sense that it accrues new lemmas slowly and even if you empty it out it will fill back up again later

[Mario Carneiro]

But I agree that it's reasonable to upstream the lemmas that are there, and I would also like to see e.g. List.attach upstream, as it would solve some dependency issues in std

[Mario Carneiro]

I think for the most part it shouldn't cause difficulties to upstream lemmas from Std.Data.List.Basic, except possibly if we want to change the names later

[Mario Carneiro]

Next, upstream the subset of Std/Data/List | Array/Lemmas.lean which are only in terms of operations already in lean4.

This is a pretty big list, it should probably be broken down into smaller pieces

[Mario Carneiro]

Is it possible to do this kind of upstreaming on an as-needed basis? The trouble with "all lemmas only about concepts in core" is that this is an unbounded list which gets added to all the time. If the list was a bit more goal directed it wouldn't have this property

[Mario Carneiro]

In particular, you will never be able to have "all the lemmas in one place"

[Kim Morrison]

Yes, I agree. But we can try. :-)

[Kim Morrison]

I'll look again at List.attach, I agree it is super useful and warrants upstreaming.

[Mario Carneiro]

FLT is a lemma only about concepts in core

[Kim Morrison]

Mario Carneiro said:

This is a pretty big list, it should probably be broken down into smaller pieces

I'll try to make a PR shortly with a proposal for what this might look like.

[Kim Morrison]

Mario Carneiro said:

FLT is a lemma only about concepts in core

Sure, but ... I think that's a bit of a strawman. :-) My basic target is "specification lemmas, simp lemmas for ext/operation combinations, lemmas describing pairwise interactions of basic operations". If you see me moving stuff that is more like FLT than that description, please slam on the brakes!

[Mario Carneiro]

Oh, another thing which should be upstreamed is setTR and other tail-recursive csimp lemmas for definitions in core

[Kim Morrison]

I think these are mostly already done?

[Yury G. Kudryashov]

Do you want it in Lean core or in the new Std library you're going to create? I'm a bit concerned about extra difficulties with fixing bugs in these files. Now I can clone std4 repo, fix a small bug, then quickly open a pr (e.g., std4#758 is about material in Data/List/Lemmas). If it will go to Lean, then it will be much harder to prepare a PR (e.g., my personal laptop is good enough to quickly compile Std but isn't good enough to build Lean).

[Kim Morrison]

We're working on this. We want to build as much as possible of the lean4 repository with lake. But I acknowledge it is harder at present.

[Kim Morrison]

Sorry about the delay on this. I have a proposed PR up at lean4#4059.