feat: fill in proof of Array.data_erase

[Seppel3210]

I also added some lemmas in List.Lemmas that were necessary.
I'm not sure about the naming of some of the lemmas I added, so I would appreciate feedback!

[Seppel3210]

awaiting-review

[Seppel3210]

Oops 🤦 Linter errors should be fixed now

[kim-em]

Otherwise looks good.

[timotree3]

I thought it was a bit ugly that this PR had to unfold morally private definitions from core like eraseIdxAux so I made a PR which would allow us to simply unfold feraseIdx instead: leanprover/lean4#3676. If that PR gets merged it will break the proofs here.

[Seppel3210]

as I said on the other PR @timotree3: In the case that your PR gets merged (and std4's lean-toolchain gets bumped) I have a commit lying around that fixes the proof https://github.com/Seppel3210/std4/commit/109c3ce97e182813a166c9b55418d9a599a01bb6

[Seppel3210]

I think it makes sense to wait for the lean4 version to get bumped since the lean4 PR was merged. Or should I PR it to the bump branch instead? (@semorrison you probably know this)

[kim-em]

Yes, if you'd like to PR to bump/v4.8.0 that's fine. It's also fine to wait: hopefully the release will be out next Tuesday.

[kim-em]

Sorry, the release was much delayed, but now should be out in the next few days again!

[Seppel3210]

hmm, the linter fail seems to be an issue with derive_functional_induction. The this it's referring to is the ignored argument in case1

[Seppel3210]

Not really sure who to ping for this issue 😅 @semorrison

[kim-em]

Let's summon @nomeata.

[nomeata]

I think the problem isn’t with feraseIdx.induct per se, but rather with rw [eraseIdx], because

diff --git a/Std/Data/Array/Lemmas.lean b/Std/Data/Array/Lemmas.lean
index 31d9a385..a56c8c5e 100644
--- a/Std/Data/Array/Lemmas.lean
+++ b/Std/Data/Array/Lemmas.lean
@@ -843,16 +843,24 @@ theorem eraseIdx_swap_data {l : Array α} (i : Nat) (lt : i + 1 < size l) :
       simp [swap_def, List.set_succ, getElem_eq_data_get]
     simp [this, ih]

+theorem feraseIdx_eq (a : Array α) (i : Fin a.size) :
+  a.feraseIdx i =
+    if h : ↑i + 1 < a.size then
+      let a' := a.swap ⟨↑i + 1, h⟩ i;
+      let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
+      a'.feraseIdx i'
+    else a.pop := by rw [feraseIdx]
+
 theorem feraseIdx_data {l : Array α} {i : Fin l.size} :
     (l.feraseIdx i).data = l.data.eraseIdx i := by
   induction l, i using feraseIdx.induct with
   | @case1 a i lt a' i' _ ih =>
-    rw [feraseIdx]
+    rw [feraseIdx_eq]
     simp [lt, ih, a', eraseIdx_swap_data i lt]
   | case2 a i lt =>
     have : i + 1 ≥ a.size := Nat.ge_of_not_lt lt
     have last : i + 1 = a.size := Nat.le_antisymm i.is_lt this
-    simp [feraseIdx, lt, List.dropLast_eq_eraseIdx last]
+    simp [feraseIdx_eq, lt, List.dropLast_eq_eraseIdx last]

 @[simp] theorem erase_data [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a := by
   let ⟨xs⟩ := l

moves the error there.

The problem is that eraseIdx.eq_1 has these unnecessary have on the right-hand side.

The proper fix that I’d advocate for is to move everything that’s only needed for the termination argument into decerasing_by, this way you get the proper equational lemma. (leanprover/lean4#4074)

If you don't want to wait with this PR until that lands, just mark the proof as nolint until this is fixed:

import Std.Tactic.Lint.Misc
…
@[nolint unusedHavesSuffices] -- until https://github.com/leanprover/lean4/pull/4074 lands

[Seppel3210]

thanks for taking a look!

[Seppel3210]

awaiting-review

[fgdorais]

Sorry for the delay following up! I just have a couple of leftover questions.