Range folds

Stream: std4

[James Gallicchio]

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]

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

[James Gallicchio]

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

[James Gallicchio]

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]

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]

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]

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

[Tomas Skrivan]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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