batteries
batteries copied to clipboard
leanprover-community
feat: fill in proof of Array.erase_data
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!
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.
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
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)
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.
Sorry, the release was much delayed, but now should be out in the next few days again!
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
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. (https://github.com/leanprover/lean4/pull/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
not sure why this is waiting on me again… I intended to push the TODO in another PR since this one is already pretty big, but I can also do it in this one I guess.