feat: add Array.eraseIdx! and some lemmas (#988)

Batteries/Data/Array/Basic.lean

@@ -172,6 +172,16 @@ greater than i.
 abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.feraseIdx ⟨i, h⟩
 
+/--
+Remove the element at a given index from an array, panics if index is out of bounds.
+-/
+def eraseIdx! (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then
+    a.feraseIdx ⟨i, h⟩
+  else
+    have : Inhabited (Array α) := ⟨a⟩
+    panic! s!"index {i} out of bounds"
+
 end Array
 
 

Batteries/Data/Array/Lemmas.lean

@@ -147,6 +147,13 @@ where
 @[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
     (l.erase a).toList = l.toList.erase a
 
+@[simp] theorem eraseIdx!_eq_eraseIdx (a : Array α) (i : Nat) :
+    a.eraseIdx! i = a.eraseIdx i := rfl
+
+@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) :
+    (a.eraseIdx i).size = if i < a.size then a.size-1 else a.size := by
+  simp only [eraseIdx]; split; simp; rfl
+
 /-! ### shrink -/
 
 theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by