feat: lemmas relating findIdx?/findFinIdx?/idxOf?/findIdxOf?/eraseP/e…

…rase on List and Array (#6864)

This PR adds lemmas relating the operations on
findIdx?/findFinIdx?/idxOf?/findIdxOf?/eraseP/erase on List and on
Array. It's preliminary to aligning the verification lemmas for
`find...` and `erase...`.

src/Init/Data/Array/Basic.lean

@@ -682,6 +682,24 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
+theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} :
+    findIdx?.loop p xs j = (findFinIdx?.loop p xs j).map (·.val) := by
+  unfold findIdx?.loop
+  unfold findFinIdx?.loop
+  split <;> rename_i h
+  case isTrue =>
+    split
+    case isTrue => simp
+    case isFalse =>
+      have : xs.size - (j + 1) < xs.size - j := Nat.sub_succ_lt_self xs.size j h
+      rw [findIdx?_loop_eq_map_findFinIdx?_loop_val (j := j + 1)]
+  case isFalse => simp
+termination_by xs.size - j
+
+theorem findIdx?_eq_map_findFinIdx?_val {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
+  simp [findIdx?, findFinIdx?, findIdx?_loop_eq_map_findFinIdx?_loop_val]
+
 @[inline]
 def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
 

src/Init/Data/List/Find.lean

@@ -886,6 +886,25 @@ theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l
     List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
   h.sublist.findIdx?_eq_none
 
+/-! ### findFinIdx? -/
+
+theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
+    List.findIdx?.go p xs i =
+      (List.findFinIdx?.go p l xs i h).map (·.val) := by
+  unfold findIdx?.go
+  unfold findFinIdx?.go
+  split <;> rename_i a xs
+  · simp_all
+  · simp only
+    split
+    · simp
+    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
+  simp [findIdx?, findFinIdx?]
+  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.
@@ -970,6 +989,12 @@ theorem idxOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
 @[deprecated idxOf?_eq_none_iff (since := "2025-01-29")]
 abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff
 
+/-! ### finIdxOf? -/
+
+theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
+    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
+  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+
 /-! ### lookup -/
 
 section lookup

src/Init/Data/List/ToArray.lean

@@ -462,4 +462,85 @@ decreasing_by
   · simp
   · simp_all [eraseIdx_eq_self.2]
 
+@[simp] theorem findIdx?_toArray {as : List α} {p : α → Bool} :
+    as.toArray.findIdx? p = as.findIdx? p := by
+  unfold Array.findIdx?
+  suffices ∀ i, i ≤ as.length →
+      Array.findIdx?.loop p as.toArray (as.length - i) =
+        (findIdx? p (as.drop  (as.length - i))).map fun j => j +  (as.length - i) by
+    specialize this as.length
+    simpa
+  intro i
+  induction i with
+  | zero => simp [findIdx?.loop]
+  | succ i ih =>
+    unfold findIdx?.loop
+    simp only [size_toArray, getElem_toArray]
+    split <;> rename_i h
+    · rw [drop_eq_getElem_cons h]
+      rw [findIdx?_cons]
+      split <;> rename_i h'
+      · simp
+      · intro w
+        have : as.length - (i + 1) + 1 = as.length - i := by omega
+        specialize ih (by omega)
+        simp only [Option.map_map, this, ih]
+        congr
+        ext
+        simp
+        omega
+    · have : as.length = 0 := by omega
+      simp_all
+
+@[simp] theorem findFinIdx?_toArray {as : List α} {p : α → Bool} :
+    as.toArray.findFinIdx? p = as.findFinIdx? p := by
+  have h := findIdx?_toArray (as := as) (p := p)
+  rw [findIdx?_eq_map_findFinIdx?_val, Array.findIdx?_eq_map_findFinIdx?_val] at h
+  rwa [Option.map_inj_right] at h
+  rintro ⟨x, hx⟩ ⟨y, hy⟩ rfl
+  simp
+
+theorem findFinIdx?_go_beq_eq_idxOfAux_toArray [BEq α]
+    {xs as : List α} {a : α} {i : Nat} {h} (w : as = xs.drop i) :
+    findFinIdx?.go (fun x => x == a) xs as i h =
+      xs.toArray.idxOfAux a i := by
+  unfold findFinIdx?.go
+  unfold idxOfAux
+  split <;> rename_i b as
+  · simp at h
+    simp [h]
+  · simp at h
+    rw [dif_pos (by simp; omega)]
+    simp only [getElem_toArray]
+    erw [getElem_drop' (j := 0)]
+    simp only [← w, getElem_cons_zero]
+    have : xs.length - (i + 1) < xs.length - i := by omega
+    rw [findFinIdx?_go_beq_eq_idxOfAux_toArray]
+    rw [← drop_drop, ← w]
+    simp
+termination_by xs.length - i
+
+@[simp] theorem finIdxOf?_toArray [BEq α] {as : List α} {a : α} :
+    as.toArray.finIdxOf? a = as.finIdxOf? a := by
+  unfold Array.finIdxOf?
+  unfold finIdxOf?
+  unfold findFinIdx?
+  rw [findFinIdx?_go_beq_eq_idxOfAux_toArray]
+  simp
+
+@[simp] theorem idxOf?_toArray [BEq α] {as : List α} {a : α} :
+    as.toArray.idxOf? a = as.idxOf? a := by
+  rw [Array.idxOf?, finIdxOf?_toArray, idxOf?_eq_map_finIdxOf?_val]
+
+@[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} :
+    as.toArray.eraseP p = (as.eraseP p).toArray := by
+  rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]
+  split <;> simp [*, findIdx?_eq_map_findFinIdx?_val]
+
+@[simp] theorem erase_toArray [BEq α] [LawfulBEq α] {as : List α} {a : α} :
+    as.toArray.erase a = (as.erase a).toArray := by
+  rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx]
+  rw [idxOf?_eq_map_finIdxOf?_val]
+  split <;> simp_all
+
 end List