Zulip Chat Archive

Stream: std4

Topic: Range folds


James Gallicchio (Oct 25 2022 at 18:28):

I'm working on the ArrayN addition to Std. In order to implement ArrayN.ofFn : (Fin n -> α) -> ArrayN α n I need a bunch of lemmas about folding over ranges with start 0 and step 1

Has anyone already written stuff in this direction? I'm trying to compare with my implementation in LeanColls to see if there's a better way.

James Gallicchio (Oct 25 2022 at 18:28):

Mainly @Tomas Skrivan; I'm not sure where it'd be located in SciLean :joy:

James Gallicchio (Oct 25 2022 at 18:31):

Relevant LeanColls implementation stuff, one of my Range folds and the resulting Array.init

James Gallicchio (Oct 25 2022 at 18:41):

My main questions are

(1) is there a generalization of my range folds, particularly foldl'', for ranges with step > 1? I've found a generalization for start > 0, but not for step > 1.

(2) how should Std include these range folds? I see three possibilities:

  • implement them on the builtin Std.Range, with proof obligations to show start = 0, step = 1
  • implement them on a new Range structure with one field stop
  • implement them as functions that just directly take a Nat (the stop value)

(3) are these range folds even necessary to implement ArrayN.ofFn cleanly?

James Gallicchio (Oct 25 2022 at 18:42):

I'm personally in favor of adding a new Range structure, but I'm not sure what to call it :P maybe SimpleRange?

Tomas Skrivan (Oct 25 2022 at 19:41):

I will look into this more closely later. Now I can point you to few places in SciLean where I do similar stuff.

Similar to Array.init, in SciLean there is: DataArray.intro. It is using for loop instead of fold and it is not really written in a way that it is easy to prove anything about it.

Similar to fold'' SciLean there is funRec but it is not using ranges at all, so probably not relevant.

James Gallicchio (Oct 25 2022 at 19:43):

Thank you for the links, I'll take a look at both!

Tomas Skrivan (Oct 25 2022 at 19:45):

To (3) can't you just initialize simple Array with a standard fold and then prove that the resulting array has size n? Instead of proving the array size at every step.

Tomas Skrivan (Oct 25 2022 at 20:01):

I'm just quickly looking at you code base and to me it looks like that having n m and h in the type of ArrayUninit is just making your time really complicated. Can't you just have a function that returns the size, the capacity and the proof(probably as axiom) for ArrayUninit?

Tomas Skrivan (Oct 25 2022 at 20:04):

The type similar to ArrayUninit is my DataArray that internally is just a ByteArray (currently is a structure with its guts open that can lead to some inconsistencies, at some point I should make it opaque or make it to a quotient)

Tomas Skrivan (Oct 25 2022 at 20:06):

Also what is the point of ArrayUninit? You can do Array.mkEmpty n which internally allocates big enough buffer such that calling n times push should be fast.

Tomas Skrivan (Oct 25 2022 at 20:11):

Ohh I see you have ArrayBuffer but you don't have many theorems about it. I think I should read your code more and think about the stuff a bit more ...

James Gallicchio (Oct 25 2022 at 20:21):

Yeah, my array hierarchy is a reimplementation of the builtin arrays, so a bunch of stuff could definitely be simpler. Not sure how necessary it was to reimplement everything, but I found it cool that I could make the C API so small :)

James Gallicchio (Oct 25 2022 at 20:22):

Tomas Skrivan said:

To (3) can't you just initialize simple Array with a standard fold and then prove that the resulting array has size n? Instead of proving the array size at every step.

Definitely -- but I ended up finding it was easier to prove inline. I'm experimenting with more abstractions now, though, so I'll see if I can get anywhere

Tomas Skrivan (Oct 25 2022 at 20:28):

I see, just when seeing the implementation of Array.init I got a huge wtf moment and it took me quite some time to understand what is going on there. Especially as the actual code it interleaved with the proof, it is hard to figure out what is what.

James Gallicchio (Oct 25 2022 at 21:23):

Definitely. I'm currently seeing if I can implement for-loop-with-loop-invariant, which would make that code way cleaner I think.

James Gallicchio (Oct 26 2022 at 22:10):

James Gallicchio said:

(1) is there a generalization of my range folds, particularly foldl'', for ranges with step > 1? I've found a generalization for start > 0, but not for step > 1.

I think I found a generalization, and one I quite like! :P
forIn with invariant: https://github.com/JamesGallicchio/std4/blob/iterators/Std/Classes/Collections/Iterable.lean#L165
relevant range implementation: https://github.com/JamesGallicchio/std4/blob/iterators/Std/Data/Range.lean

James Gallicchio (Oct 26 2022 at 22:10):

the types are like super ugly but I think with enough syntax sugar it could look equivalent to Why3/Dafny stuff


Last updated: Dec 20 2023 at 11:08 UTC