-
Notifications
You must be signed in to change notification settings - Fork 87
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: fill in proof of Array.erase_data #690
base: main
Are you sure you want to change the base?
Conversation
awaiting-review |
I also added some lemmas in List.Lemmas that were necessary
Oops 🤦 Linter errors should be fixed now |
Otherwise looks good. |
Std/Data/Array/Lemmas.lean
Outdated
erase_none {xs : List α} (i : Nat) (h : List.indexOf? a xs = none) : | ||
xs.drop i = (xs.drop i).erase a := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can erase_none
be factored into these three more generally useful lemmas?
theorem erase_eq_of_nmem : x ∉ xs -> xs.erase x = xs := sorry
theorem nmem_drop_of_nmem : x ∉ xs -> x ∉ xs.drop i := sorry
theorem indexOf?_eq_none_iff : List.indexOf? x xs = none ↔ x ∉ xs := sorry
I thought it was a bit ugly that this PR had to unfold morally private definitions from core like |
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 Seppel3210@109c3ce |
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 |
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 |
Not really sure who to ping for this issue 😅 @semorrison |
Let's summon @nomeata. |
I think the problem isn’t with 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 The proper fix that I’d advocate for is to move everything that’s only needed for the termination argument into If you don't want to wait with this PR until that lands, just mark the proof as
|
otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into `decreasing_by`, the equational theorems are unencumbered by termination arguments. see also leanprover-community/batteries#690 (comment)
otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into `decreasing_by`, the equational theorems are unencumbered by termination arguments. see also leanprover-community/batteries#690 (comment)
should be good now @semorrison |
awaiting-review |
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!