Arrays of size `n`, where `n` is constant and small

Stream: Is there code for X?

[Hanting Zhang]

I have some theorems involving Arrays with small and constant sizes, which I need to reason about. What would be the best way to prove a lemma like this?

theorem Array.of_size_eq_4 (arr : Array α) (h : arr.size = 4) :
  arr = #[arr[0], arr[1], arr[2], arr[3]] :=
by
  sorry

My best attempt so far is:

lemma Array.of_size_eq_4 (arr : Array α) (h : arr.size = 4) :
  arr = #[arr[0], arr[1], arr[2], arr[3]] :=
by
  ext i hi hi'
  · simp [h]
  ·
    sorry

At the sorry I could bash cases for i = 0, 1, 2, 3... but I feel like there must be a better (or at least shorter) way. I recall there being a tactic that helps with going through every possible value of a number in a range and case-bashing?

[Kyle Miller]

import Mathlib

lemma Array.of_size_eq_4 (arr : Array α) (h : arr.size = 4) :
  arr = #[arr[0], arr[1], arr[2], arr[3]] :=
by
  ext i hi hi'
  · exact h
  · rw [h] at hi
    interval_cases i <;> rfl

[Hanting Zhang]

:O interval_cases was exactly it, thanks!

[Hanting Zhang]

Continuation:

Is it just me that can't find them, or is Batteries direly missing a ton of Array/Subarray lemmas? :sob:

[Kim Morrison]

@Hanting Zhang, you can also use docs#Vector. Lemma coverage for Array and Vector mostly lives in the core Lean distribution now, so don't go looking in Batteries for this. Coverage has significantly increased over the last two months, so please check out v4.17.0-rc1 when it lands next monday or tuesday. (Or just the nightlies.)

If you have specific things you're looking for in Array, please tell me directly about it. We know that Subarray is direly underspecified at present, but this isn't happening immediately. Contributions for Subarray are very welcome at Batteries, or talk to me if you're interested in doing more comprehensive work on Subarray directly via PRs to Lean.

[Kyle Miller]

By the way, there turns out to be a very short proof of the lemma @Hanting Zhang that makes use of match's ability to use h to see the cases are exhaustive.

lemma Array.of_size_eq_4 (arr : Array α) (h : arr.size = 4) :
    arr = #[arr[0], arr[1], arr[2], arr[3]] :=
  match arr, h with
  | ⟨[_,_,_,_]⟩, _ => rfl

[Hanting Zhang]

Hmm, the compiler is crazy.

@Kim Morrison: Thanks for the info -- I can see the PRs for lean4#6864, lean4#6868, etc :eyes:. I've always wanted to help with Mathlib/Batteries, so I'd love to talk about more comprehensive contributions -- although probably on a sporadic schedule since I won't have bandwidth to do so consistently. Let me know what works for you!