Zulip Chat Archive
Stream: Is there code for X?
Topic: Array sorting.
Wrenna Robson (Jun 05 2025 at 09:52):
We have various functions which sort Arrays in various ways. Do any of them have a proof that the resulting Array is indeed sorted?
Kim Morrison (Jun 05 2025 at 10:28):
See docs#List.sorted_mergeSort
Wrenna Robson (Jun 05 2025 at 10:29):
Right, but is that linked, say, to Array.qsort
Wrenna Robson (Jun 05 2025 at 10:30):
Or indeed Array.merge.
Kim Morrison (Jun 05 2025 at 10:30):
There is also Array.qsort_sorted, but it currently lives in tests/lean/run/grind_qsort.lean.
Wrenna Robson (Jun 05 2025 at 10:31):
That does sound like the kind of thing you'd want!
Kim Morrison (Jun 05 2025 at 10:31):
(We will change the definition of qsort at some point, so for now that verification code is just a grind test case rather than library code.)
Wrenna Robson (Jun 05 2025 at 10:31):
Vector.sort would be quite nice as well.
Wrenna Robson (Jun 05 2025 at 10:33):
Huh, while I'm here: does getElem_unzip_fst or similar exist?
Wrenna Robson (Jun 05 2025 at 10:34):
(For Array or Vector.)
Aaron Liu (Jun 05 2025 at 10:58):
I guess you could use docs#Array.fst_unzip plus docs#Array.getElem_map
Wrenna Robson (Jun 05 2025 at 10:59):
Yes, that's probably what works, doesn't it.
Aaron Liu (Jun 05 2025 at 11:01):
But I don't think it would play well with rw on getElem because of the bounds proof
Wrenna Robson (Jun 05 2025 at 11:02):
Certainly I find it is always nice to just have a getElem lemma if you can.
Kim Morrison (Jun 05 2025 at 11:07):
Yes, I'd be happy to have that. Interested in PRing it?
Kim Morrison (Jun 05 2025 at 11:07):
You could even mark it as @[grind =].
Wrenna Robson (Jun 05 2025 at 11:08):
Happy to do so. Into lean4, right? Anything special I should remember about PRing there?
Kim Morrison (Jun 05 2025 at 11:08):
The build instructions are kind of complicated still. Apologies if you haven't jumped through those hoops yet... We're working on it.
Wrenna Robson (Jun 05 2025 at 11:08):
Well, I guess for comparison, I submitted lean#8406 the other day - is that the right kind of form?
Wrenna Robson (Jun 05 2025 at 11:08):
I just about managed to build it!
Kim Morrison (Jun 05 2025 at 11:08):
Kim Morrison (Jun 05 2025 at 11:13):
@Wrenna Robson, I left some comments there. Please ping me here when you've responded/fixed.
Kim Morrison (Jun 05 2025 at 11:14):
(Thank you, these look good.)
Wrenna Robson (Jun 05 2025 at 11:14):
Oh! Happy to, sorry, didn't intend to ask you for a review there :) - once I get building working on this machine I will get right on it.
Wrenna Robson (Jun 05 2025 at 11:17):
I had the pleasure of having a lot of lemmas like this in my personal repository which your team one-by-one added themselves over time - was lovely to see. But a few remained.
Wrenna Robson (Jun 05 2025 at 13:26):
@Kim Morrison have addressed all your issues I believe (and merged master in).
Wrenna Robson (Jun 05 2025 at 14:44):
I have a core development question: I have edited one file imported by another, but new theorems introduced in the first file don't seem to appear in the second. How do I update/rebuild that first file
Wrenna Robson (Jun 05 2025 at 14:45):
Running the build script again seems to work... is this really the best way?
Henrik Böving (Jun 05 2025 at 15:41):
Yes
Wrenna Robson (Jun 05 2025 at 17:41):
@Kim Morrison also, lean4#8644
Wrenna Robson (Jun 05 2025 at 23:28):
... which Eric has commented on telling me it isn't needed. I take his point - that simp can handle all these lemmas might mean they aren't needed - but to me it's somewhat unnatural to not have some kind of getElem lemma here. And you did say I ought to do it.
Wrenna Robson (Jun 05 2025 at 23:29):
I wasn't quite sure which ones I should mark as @[grind =] though.
Last updated: Dec 20 2025 at 21:32 UTC