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?
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 !