2
$\begingroup$

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?

$\endgroup$
1

2 Answers 2

2
$\begingroup$

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
$\endgroup$
0
1
$\begingroup$

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
$\endgroup$
5
  • $\begingroup$ I don't understand ... so what, basically we can't use arrays ?? $\endgroup$
    – redjamjar
    Commented Oct 10, 2023 at 20:02
  • 1
    $\begingroup$ @redjamjar: You can use arrays, but only in safe ways. $\endgroup$ Commented Oct 10, 2023 at 20:54
  • 1
    $\begingroup$ @redjamjar you can write programs with arrays, but you can't reason about them. $\endgroup$
    – ice1000
    Commented Oct 10, 2023 at 21:23
  • $\begingroup$ @ice1000: Would you really say that? If you provide proofs of correctness of indices, as you should, you can reason about arrays. $\endgroup$ Commented Oct 11, 2023 at 5:34
  • 1
    $\begingroup$ @AndrejBauer you're right. I should say you can't reason about them as naturally as you could reason about lists -- you would pay extra effort to do so. $\endgroup$
    – ice1000
    Commented Oct 11, 2023 at 6:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.