porting `.array` files whose PR's were closed?

Stream: mathlib4

[Thomas Murrills]

I thought I'd try to port logic.equiv.array since it's at the top of the #port-dashboard and we're now choosing to align array with Array as per this message, only to find that the branch and PR already exist, but were closed: !4#1733.

[Thomas Murrills]

Is reopening the PR and changing the Array' that appears there to Array the right move? Just wanted to confirm.

[Thomas Murrills]

(The situation is similar for data.array.lemmas (!4#2194))

[Scott Morrison]

Sounds good! Sorry for the confusion. :-)

[Thomas Murrills]

No problem! (Sorry if this was addressed in the meeting; I thought it would be quicker to ask on zulip since I couldn't make it today! :) ...Though, I did just realize the meeting recording has a searchable transcript, which would have made finding a mention of it way easier than I thought. :upside_down:)

[Thomas Murrills]

Okay, a couple clarifying questions:

1. we have both DArray and Array' floating around in these files, DArray being a heterogeneous array. Is DArray also meant to be aligned to Array? (That seems like it might be a bigger semantic gap!)

2. What should the type signature of something like def arrayEquivFin (n : ℕ) (α : Type _) : Array' n α ≃ (Fin n → α) become? Array α ≃ (n : ℕ) × (Fin n → α), or { a : Array α // a.size = n } ≃ (Fin n → α), or both, or neither?

[Scott Morrison]

As far as I'm aware, DArray doesn't exist yet anywhere. I would be inclined to just #noalign these, with a comment that DArray doesn't exist yet.

[Scott Morrison]

I would be inclined to #noalign lemmas about Array' too, perhaps with a note that users should use Vector instead. (Perhaps even hinting that we've thought about changing the implementation of Vector to be in terms of Array rather than List.)

[James Gallicchio]

do we want any of the mathlib3 array stuff to be persisted..? I was under the impression that it's not worth persisting

[Scott Morrison]

What do you mean by persisted?

[Scott Morrison]

Our conclusion in the porting meeting today that anything about the old array which still makes sense in terms of the new Array should be ported.

[Scott Morrison]

For the sake of the port these results should just go in a file corresponding to the original mathlib3 location. After the port we can rationalize.

[Thomas Murrills]

Hmm, okay. I guess the question is then, "where's the line past which translating Array' to Array doesn't make sense". I guess...#noalign if we need to mention the size of the array in the type?

[Scott Morrison]

Array' is essentially Vector. It is not Array, but something more complicated. I would suggest everything about Array' gets #noalign'd, and if you like add a porting note explaining the users should use Vector rather than Array'. Without some evidence that there actually exist users interested in Array', I wouldn't do more than that.

[James Gallicchio]

I am adding a dependent/heterogeneous array, and a fixed-length array (iso to Vector) to Std at some point, but I need a pretty minimal API for my use case so I suspect it's not worth putting much effort into porting the non-array stuff.

[James Gallicchio]

plus all the proofs will be broken since the implementation will not be the same :)

[Thomas Murrills]

Scott Morrison said:

Array' is essentially Vector. It is not Array, but something more complicated. I would suggest everything about Array' gets #noalign'd, and if you like add a porting note explaining the users should use Vector rather than Array'. Without some evidence that there actually exist users interested in Array', I wouldn't do more than that.

Right, no, I understand the difference, but I thought the point of what was said at the porting meeting was to rewrite theorems about array( = Array') that make sense for Array and #noalign things which don’t, not to simply #noalign everything about Array'.

The issue is that you can find a natural way to make some theorems about array/Array' make sense for Array by forgetting the size information appropriately, e.g. Array' n α \equiv Fin n → α can become Array α \equiv ((n : ℕ) × (Fin n → α)), or by retaining the size information, by replacing Array' n α with { a : Array α // a.size = n }. So the question is essentially “how much rewriting do we do”.

I suppose the most obvious thing is to just rewrite the things for which we can sensibly drop in Array α for Array n α nearly verbatim, like the Traversable instance, especially given James’ incoming Std types?

[James Gallicchio]

Where were these lemmas used in mathlib, out of curiosity?

[James Gallicchio]

One of the issues with the current collection lemmas is we have copied large swaths of lemmas from one collection to another in very repetitive style -- I was hoping to standardize most of these lemmas around models (List/Multiset/Finset/[FinEnum A] \x (A -> B)) to cut down the repetition and get a big set of lemmas for each collection for free.

These alternative arrays from mathlib3 have the same property that many collections do, where they can be viewed through the lens of multiple different models that each give different lemmas. I imagine that is what you are referring to when you say some of the lemmas can be generalized in multiple ways.

TL;DR I wouldn't really worry about porting lemmas that already exist on e.g. List -- but if there are lemmas that don't mirror those in a different collection, I would be interested!!

[James Gallicchio]

And if you don't feel like trying to sort out which ones are already present on List, I personally think it's fine to just not port them if they're not being used elsewhere. We can always look back at the lean3 source if we want to later.

[James Gallicchio]

But I also don't know what the rationale was at the porting meeting, so maybe there is a good reason to port them after all :joy:

[Scott Morrison]

Oh, I'm an idiot, I have just been completely forgetting that Lean3's array had the length as a parameter. Ignore everything I've been saying. :-)

[Scott Morrison]

I have revised my position to: junk it all. :-)

[Thomas Murrills]

Oh, okay! Sounds good! :D

[Thomas Murrills]

Though, maybe we ought to include the standard equivalence Array α ≃ List α in that file. Surprisingly, I couldn't find this equivalence elsewhere already. (Did I miss it?) This lets us include Array.encodable and Array.countable easily, and is kind of the "moral port" of this file, in a way—it's also what you'd expect if you didn't know about mathlib3 and stumbled on a file called "Logic.Equiv.Array" :)

[James Gallicchio]

I think the necessary lemmas for it are proven somewhere in Std. No clue if the equivalence is in Std.

[Thomas Murrills]

I searched for ≃ List and ≃ Array in Std, and checked the autocomplete list for arrayEquiv and listEquiv while importing Std, so I'm pretty sure it isn't! I pushed a commit adding it, and if we don't like it (or don't like doing stuff like that during the port), we can easily revert the relevant commit or put it somewhere else :)

[Mario Carneiro]

std doesn't have Equiv, so it is not too surprising the first search fails

[Mario Carneiro]

And there is nothing to prove regarding equivalence of List and array, one is literally a wrapper for the other so the lemmas you would need to apply are all autogenerated

[Mario Carneiro]

I think the proof is just \<Array.mk, Array.data, fun | rfl => rfl, fun | rfl => rfl\>

[Thomas Murrills]

Oh, yeah, that's nicer than what I wrote, which was in terms of toArray and toList.

[Thomas Murrills]

And, ah, I thought lean core had equiv since it comes up in searches, but those are all in test files :)

[Thomas Murrills]

I also commented out the instances for Traversable (Array α) and IsLawfulTraversable (Array α) and added the following porting note explaining the rationale:

Porting note: removed instances for what would be ported as Traversable (Array α) and IsLawfulTraversable (Array α). Since Array is now a core datatype, these would
1. be implemented directly in terms of Array functionality for efficiency, rather than being the traversal of some other type transported along an equivalence to Array α (as the traversable instance for array was)
2. belong in Mathlib.Control.Traversable.Instances instead of this file.

Again, we can revert that commit or change it if it's inaccurate, but I thought I'd provide an actionable option to try to move things along :)

[Mario Carneiro]

Since Array is now a core datatype

Actually Array was always a core datatype, we just cared less about this kind of thing in lean 3

[Thomas Murrills]

"Since we now care more about Array as a datatype", maybe? EDIT: kept it simple and just deleted the line, leaving "These would".

[Thomas Murrills]

Ok, I've put !4#1733 out for review; if we want to change anything we can do so in the review stage :)

[Ruben Van de Velde]

Scott Morrison said:

Our conclusion in the porting meeting today that anything about the old array which still makes sense in terms of the new Array should be ported.

I'm quite surprised by this. array n α shares nothing but a name with Array α, so this isn't so much porting as it is adding new API for a new data structure. As far as I can tell, Array α is just an optimized List α, while array n α corresponds more closely to Vector α n in having the length in encoded in the type

[Johan Commelin]

Scott Morrison said:

I have revised my position to: junk it all. :-)

:this:

[Ruben Van de Velde]

So what happened to #1733 and why is #2194 still open?

[Johan Commelin]

Those are good questions :sweat_smile:

[Thomas Murrills]

One argument is: if we do have a file called Array in the mathlib4, it ought to refer to Array. In some cases we can translate the statements about array to Array, so let's "port" those definitions in the files named "array" by replacing them with the corresponding ones for Array. In the cases where we can't easily adapt the definitions, junk them and leave a porting note.

We don't just align array to Vector because vector already existed in mathlib (I believe) and is already aligned to it, and was implemented differently, so that only leaves us #noaligning or aligning with Array. Since they are at least somewhat-related types, and we don't want to just lose theorems if we don't have to, we can just try to ride out the semantic difference and align the array theorems to the adapted Array theorems where possible. So, that means #2194 ought to be (mostly) dealt with by aligning to corresponding Std theorems about Array, and adapting or junking the rest.

...That's what I understand the reasoning to be, in any case. There's definitely an argument for saying "actually, let's just start fresh" too :)

[Eric Wieser]

Just to throw another opinion in here: I think we should either:

1. Junk it all (edit: via #noalign)
2. Blindly port it as Array' (which I think is what #2194 does) so that we can really claim "everything in mathlib3 is available in mathlib4", then junk it later down the line (perhaps merging the results with the stuff in Mathlib.Data.Fin.Tuple?)

[Ruben Van de Velde]

I'd noalign everything

[Mario Carneiro]

I think Array' will be coming back at some point once the DArray work in std is finished

[Eric Wieser]

So is your vote that we do my point 2 above?

[Johan Commelin]

I vote for option 1.

[Mario Carneiro]

I think my point is in favor of "do nothing for now, revisit this later"

[Mario Carneiro]

where "do nothing" can also be interpreted as "#noalign / port empty files / otherwise count the files as ported"

[Matthew Ballard]

I think 1 sounds good until we know the final version of DArray

[Matthew Ballard]

#5821 if that is what we want to do