Return to Answer

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
```

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

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 this 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```

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 
```

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 4 options here:

• if you use the a[i]! notation, you won't be able to prove your theorem since lean won't reduce this.
• 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 this 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```

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 this 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```