This array lemma should be easier!?

Stream: general

[François G. Dorais]

I would have expected this theorem to be easier to state and prove. I'm probably missing something. Ideas?

theorem Array.getElem_append (as bs : Array α) (i) (hi : i < (as ++ bs).size) :
    (as ++ bs)[i] = if h : i < as.size then as[i] else
      have : i - as.size < bs.size := by
        apply Nat.sub_lt_left_of_lt_add
        · exact Nat.le_of_not_gt h
        · rw [← size_append]; exact hi
      bs[i - as.size] := by
  rw [getElem_eq_data_getElem]
  conv => lhs; arg 1; rw [append_data]
  split
  · rw [List.getElem_append_left]; rfl
  · next h =>
    rw [List.getElem_append_right]
    rw [size_eq_length_data] at h; rfl
    exact h

[MohanadAhmed]

Are you trying to simplify the statement or the proof body?
If the later maybe the theorems [get_append_left and `get_append_right] might be useful?

[MohanadAhmed]

theorem Array.getElem_append (as bs : Array α) (i) (hi : i < (as ++ bs).size) :
    (as ++ bs)[i] = if h : i < as.size then as[i] else
      have : i - as.size < bs.size := by
        apply Nat.sub_lt_left_of_lt_add
        · exact Nat.le_of_not_gt h
        · rw [← size_append]; exact hi
      bs[i - as.size] := by
  split
  rw [get_append_left]
  next h =>
  rw [get_append_right];
  exact Nat.le_of_not_lt h

[Daniel Weber]

Perhaps docs#tacticGet_elem_tactic_trivial should know to use docs#Array.size_append

[Daniel Weber]

attribute [simp] Array.size_append

macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| simp_all (config := { arith := true }); try omega; done)

theorem Array.getElem_append (as bs : Array α) (i) (hi : i < (as ++ bs).size) :
    (as ++ bs)[i] = if h : i < as.size then as[i] else bs[i - as.size] := by
  split
  · rw [get_append_left]
  · rw [get_append_right]
    omega

[Yury G. Kudryashov]

I think that it should use a non default simp set. Also, it shouldn't use simp all, because having h : a = a + b - c in context shouldn't break it.