Meaningful fields for Subarray

[fgdorais]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The current Subarray structure has cryptic field names:

structure Subarray (α : Type u)  where
  as : Array α
  start : Nat
  stop : Nat
  h₁ : start ≤ stop
  h₂ : stop ≤ as.size

I propose the following alternative with more intuitive field names:

structure Subarray (α : Type u) extends Array α where
  start : Nat
  stop : Nat
  valid : start ≤ stop ∧ stop ≤ toArray.size

I have a potential PR candidate implementing this: https://github.com/fgdorais/lean4/tree/subarray

[fgdorais]

An alternative with a simpler validity condition would be:

structure Subarray (α : Type u) extends Array α where
  start : Nat
  size  : Nat
  valid : start + size ≤ toArray.size

abbrev Subarray.stop (as : Subarray α) : Nat := as.start + as.size