Skip to content

Commit

Permalink
feat: prove Array.toList_erase
Browse files Browse the repository at this point in the history
  • Loading branch information
mehbark committed Jan 28, 2025
1 parent 3831375 commit a288bf4
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions Batteries/Data/Array/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,10 @@ where

/-! ### erase -/

@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
(l.erase a).toList = l.toList.erase a
@[simp] theorem toList_erase [BEq α] {l : Array α} {a : α} :
(l.erase a).toList = l.toList.erase a := by
simp [erase, ← List.eraseIdx_indexOf_eq_erase, List.indexOf_eq_indexOf?]
cases h : l.indexOf? a <;> simp [Array.indexOf?_toList, List.eraseIdx_of_length_le, *]

@[simp] theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) :
(a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by
Expand Down

0 comments on commit a288bf4

Please sign in to comment.