Definition of subarray

Stream: lean4

[Johannes Tantow]

Hi,
I am currently working with Subarray to prove the correctness of some algorithm and find it a bit tedious to work with. As a background the problem deals with finding the optimal subarray of some given array a and criteria.

I very often need to add s.array = a to my theorem statements, because the Subarray only receives the type and hence there might be a different array a' with some better subarray. A more clean definition for my use case would be the following:

structure Subarray' {α : Type _} (a : Array α) where
  start : Nat
  stop : Nat
  /--
  The starting index is no later than the ending index.

  The ending index is exclusive. If the starting and ending indices are equal, then the subarray is
  empty.
  -/
  start_le_stop : start ≤ stop
  /-- The stopping index is no later than the end of the array.

  The ending index is exclusive. If it is equal to the size of the array, then the last element of
  the array is in the subarray.
  -/
  stop_le_array_size : stop ≤ as.size

def Subarray'.array {α : Type _} {a : Array α} (_ : Subarray' a) := a

The Subarray.array method looks then a bit strange with the anonymous subarray, but I think the rest should work the same as previously.

Is there some alternative reason that makes this definition better to use or is it better on a low-level memory aspect? If not I would propose to change it and can also create the PR. I also looked in mathlib and batteries and at least with githubs search didn't find any usecase where this would lead to large fallout (or any large use of it).

[Markus Himmel]

We will completely overhaul Subarray in the next few months, so I'm afraid right now would not be a good time to make a PR. Thanks a lot for writing down your experience, we will be taking this into account for the new design.

[Johannes Tantow]

I guess I can also for now just define my own subarray instance and work with that. I mainly use it to bundle the information better, so that works for me for now.

[Tomas Skrivan]

I think currently Subarray does not have API for mutation but I'm not even sure if it would be possible to do for your definition of subarray.

[Johannes Tantow]

I don't see why it shouldn't be possible though one might have to use cast in the definition when the underlying array changes.
I guess the design mainly depends though on what you want to do with it. I am not really interested in having subarrays of different arrays to have the same type.