Simplifying Array Access

Question

I'm confused how to show the second example here:

example (n:Nat): [n][0] = n := 
by
  simp

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

I tried a few different ways without success. The first is fine since we're using a List rather than an Array. What did I miss?

Answer 1

The error you get when writing that example should guide you in understanding how to solve your issue:

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
n: Nat
⊢ 0 < Array.size #[n]

You have 3 possible options here:

• if you use the a[i]! notation, you won't be able to prove your theorem since lean won't reduce this. This won't work.
• you may use a[i]? to prove that #[n][0]? = some n instead
• additionally, you could provide a proof that your 0 index is a valid index in this case.

In practice, the best way to do this would be to teach Lean that your index is indeed correct. You can do so by providing simp lemmas for this. The following code works:

-- Works without adding a lemma
example (n:Nat): #[n][0]? = some n := rfl

-- We can manually provide a proof that `0 < #[n].size` 
example (n:Nat): #[n][0]'(Nat.lt_succ_self 0) = n := rfl

-- Alternatively, we can provide that proof to `simp` by tagging the theorem as such
@[simp]
theorem zero_lt_array_one : 0 < #[a].size := Nat.lt_succ_self 0

-- No need to provide a proof now, it just works !
example (n:Nat): #[n][0] = n := rfl

Alternatively, you could just import the standard library, which provides everything lean needs to know such array access is well-behaved:

import Std

example (n:Nat): #[n][0] = n := rfl

Answer 2

I think Lean 4 is intended to not reduce Array-related stuffs:

The Lean type checker has no special support for reducing Arrays.

From: https://lean-lang.org/lean4/doc/array.html

By some analysis, we can see that Lean refuses to calculate the size of #[n]:

example (n: Nat):
  let x := #[n];
  let ix : Fin x.size := 0;
  x[ix] = n :=
by
  sorry

The definition ix also raises error, but it makes the following code type check.

However, you can postulate a proof that 0 < x.size:

example (n: Nat):
  let x := #[n];
  let h : 0 < x.size := by sorry;
  x[0] = n :=
by
  trivial