how to show index access is valid

Stream: new members

[Asei Inoue]

I tried defining the Array.reverse function in an imperative style, but I couldn't prove that the array accesses are valid. How can I make the proof go through?

def Array.reverse' {α : Type} (arr : Array α) : Array α := Id.run do
  let mut array : Array α := arr
  let size := array.size
  for h : i in [0 : size / 2] do
    have : i < array.size := by
      dsimp [(· ∈ ·)] at h
      simp at h
      simp [size] at h
      /- α : Type
      arr : Array α
      array✝ : Array α := arr
      size : Nat := array✝.size
      i : Nat
      r✝ : Array α
      array : Array α := r✝
      h : i < array✝.size / 2 ∧ i % 1 = 0
      ⊢ i < array.size -/
      sorry
    array := array.swap i (size - 1 - i)
  return array

[Aaron Liu]

Use Vector instead which prevents you from changing the length of the array while inside the loop

[Aaron Liu]

You can use docs#Array.toVector to get the initial vector and you can use docs#Vector.toArray to get an array out at the end

[Asei Inoue]

(deleted)

[Asei Inoue]

:)

def Array.myReverse' (arr : Array α) : Array α := Id.run do
  let mut vec := arr.toVector
  let size := vec.size
  for h : i in [0 : size / 2] do
    have : i < vec.size := by
      dsimp [(· ∈ ·)] at h
      grind
    have : size - 1 - i < vec.size := by
      dsimp [(· ∈ ·)] at h
      grind
    vec := vec.swap i (size - 1 - i)
  return vec.toArray

[Aaron Liu]

just grind again

def Array.myReverse' (arr : Array α) : Array α := Id.run do
  let mut vec := arr.toVector
  let size := vec.size
  for h : i in [0 : size / 2] do
    have : i < size := by
      dsimp [(· ∈ ·)] at h
      grind
    vec := vec.swap i (size - 1 - i) (by grind) (by grind)
  return vec.toArray

[Asei Inoue]

I think get_elem_tactic should call grind internally

[Aaron Liu]

a lot of these tactics are supposed to fail fast

[Asei Inoue]

@Aaron Liu Thank you!

[Asei Inoue]

@Aaron Liu

I think get_elem_tactic should call grind internally

How about using grind +timeout with a setting that immediately terminates if it doesn't finish within 0.5 seconds?