feat: getElem!_cons_zero

[mo271]

No description provided.

[fgdorais]

Nice! Lean core has List.cons_getElem_zero and List.cons_getElem_succ, so following the same convention makes sense here. Also, you might as well add all the companion theorems at the same time:

@[simp] theorem cons_getElem!_zero [Inhabited α] {as : List α} : (a :: as)[0]! = a := by
  unfold getElem!; simp [Nat.zero_lt_succ]

@[simp] theorem cons_getElem!_succ [Inhabited α] {as : List α} : (a :: as)[i+1]! = as[i]! := by
  unfold getElem!; split
  next h => rw [dif_pos (Nat.lt_of_succ_lt_succ h)]; rfl
  next h => rw [dif_neg (mt Nat.succ_lt_succ h)]

@[simp] theorem cons_getElem?_zero {as : List α} : (a :: as)[0]? = a := by
  unfold getElem?; simp [Nat.zero_lt_succ]

@[simp] theorem cons_getElem?_succ {as : List α} : (a :: as)[i+1]? = as[i]? := by
  unfold getElem?; split
  next h => rw [dif_pos (Nat.lt_of_succ_lt_succ h)]; rfl
  next h => rw [dif_neg (mt Nat.succ_lt_succ h)]

[mo271]

Great, I added the lemmas you suggested.
Just above we have get_cons_zero. Should this be changed (perhaps in a separate pull request) to cons_get_zero for more consistent naming?

[mo271]

Without removing the simps I got a lint error:
https://github.com/leanprover/std4/actions/runs/5806195289/job/15738605134?pr=214

[fgdorais]

I think get_cons_zero is fine. I think getElem is reversed because it's a postfix operator.

The simp lint error is interesting: it appears that the simp normal form for lists is to change getElem and getElem? to List.get and List.get?, respectively. This works fine since there is a large API for List.get and List.get? that was inherited from Lean 3. Unfortunately, the List.get! API is not nearly as well developed, so that translation doesn't work so well for getElem!.

[mo271]

Regarding the simp lint error:
Is there anything we should do to address this in this pull request or is it good to go?

If I understand correctly, we should add lemma like getElem!_eq_get! and then the simp linter will also fire for cons_getElem!_zero and cons_getElem!_succ, so then we also remove the simp attribute there.

[fgdorais]

I think it's fine as-is. getElem!_eq_get! wouldn't be useful since there aren't enough lemmas about get!. In the future, once there are enough getElem lemmas, the simp normal form might reverse toward getElem form. Time will tell.

[digama0]

I don't like these lemmas, because getElem? and getElem! on list are not simp-normal, the .get / .get? function is preferred. For panicking functions the simp normal form would be something like .getD default. (The reason for this is because even though getElem? has a cleaner syntax, it doesn't have very good defeqs compared to get?.) We should not encourage having two ways to say the same thing as this squares the number of required lemmas (since every preferred spelling has to interact with every other preferred spelling).

[mo271]

ok, let's close this pull request then, I suppose...