chore: replace custom List.slice with upstream List.extract - #885
chore: replace custom List.slice with upstream List.extract#885oliver-butterley wants to merge 8 commits into
Conversation
|
Thanks for this! Yes, this is the appropriate workflow for deprecation. On a side note: I need to check that some internal projects still build before merging this PR. |
Yes, very wise check! On our side I'll just see what happens and hope that our infrastructure is sufficiently robust that my colleagues deal with possible issues without any pain! 🤣 |
There was a problem hiding this comment.
This looks good to me! There are a few renamed Slice lemmas that weren't aded to the deprecation list. I'm not sure if it's super important, but it's the only thing I noticed. (looking closer I actually didn't catch everything, everything looks good to me!)
| @[simp, simp_lists_safe, grind =] | ||
| theorem getElem?_slice (i j k : Nat) (ls : List α) | ||
| theorem getElem?_extract (i j k : Nat) (ls : List α) | ||
| (_ : j ≤ ls.length ∧ i + k < j) : | ||
| (ls.slice i j)[k]? = ls[i + k]? := by | ||
| revert i j | ||
| induction ls | ||
| . intro i j; simp_all | ||
| . intro i j h | ||
| simp_all [slice] | ||
| have : k < j - i := by scalar_tac | ||
| simp [*] | ||
| (ls.extract i j)[k]? = ls[i + k]? := by grind |
There was a problem hiding this comment.
Do we actually still need this theorem (as grind solves the goal)?
In particular: I'm wondering whether we should mark it as grind =
It is very likely that we just need to mark a Lean std lemma with simp_lists_safe
| (ls.slice i j)[k]! = ls[i + k]! := by | ||
| have := getElem?_slice i j k ls | ||
| simp_all | ||
| (ls.extract i j)[k]! = ls[i + k]! := by grind |
| have h1 := getElem?_slice i j k ls (by grind) | ||
| rw [getElem?_eq_getElem hk, getElem?_eq_getElem hik] at h1 | ||
| exact Option.some.inj h1 | ||
| (ls.extract i j)[k] = ls[i + k] := by grind |
oliver-butterley
added
the
awaiting author
3 participants
List.slice -> List.extract refactor
Replaced the custom List.slice definition with Lean's built-in List.extract (identical semantics, different arg order: slice start stop ls -> ls.extract start stop).
Changes:
fixes #814