Reducing Array Initialisers

Question

I am trying to show the following:

example (n:Nat): #[n][0] = n := 
by
  sorry

Whilst the equivalent is easy to show for lists, I understand that reducing Arrays is problematic in Lean4. But, I still want to show it. So, I'm trying various things, such as the following:

example (n:Nat)(arr: Array Nat)(p:arr=#[n]): #[n][0] = n := 
by
  rw [<-p]

Logically, this makes sense to me. But, a mysterious error is given:

tactic 'rewrite' failed, motive is not type correct

I haven't seen this before! So, then I try something even more verbose:

example (n:Nat)(arr: Array Nat)(p:arr.data = [n])(i:Fin arr.size): arr[i] = n := 
by
  have p: arr.data.length = 1 := by simp [*];
  have q: i.val = 0 := (by linarith [i.isLt]);
  unfold Array.get

And now its complaining that failed to unfold 'Array.get'. I don't understand how it can fail to unfold?

Overall, my conclusion is that arrays should be avoided. Thoughts?

Answer 1

The real issue you're encountering is the fact that #[n] doesn't outright mean Array.mk [n], it is elaborated as List.toArray, which is better optimised, but also harder to reason about. Your best bet to solve such examples would be to simply use rfl. Arrays are computational, and #[n][0] will reduce to n with no issue, you can verify it using

variable (n : Nat)

#reduce #[n][0] --n

Make use of definitional equality when you can, it's a powerful tool !