From fa4cd6d78cce7f638788d3f0badc1cfba720eb4b Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 28 Jan 2026 15:55:29 +1100
Subject: [PATCH] feat: add theorems relating find? with findIdx? and
 findFinIdx? (#12204)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds theorems showing the consistency between `find?` and the
various index-finding functions. The theorems establish bidirectional
relationships between finding elements and finding their indices.

**Forward direction** (find? in terms of index):
- `find?_eq_map_findFinIdx?_getElem`: `xs.find? p = (xs.findFinIdx?
p).map (xs[·])`
- `find?_eq_bind_findIdx?_getElem?`: `xs.find? p = (xs.findIdx? p).bind
(xs[·]?)`
- `find?_eq_getElem?_findIdx`: `xs.find? p = xs[xs.findIdx p]?`

**Reverse direction** (index in terms of find?):
- `findIdx?_eq_bind_find?_idxOf?`: `xs.findIdx? p = (xs.find? p).bind
(xs.idxOf?)`
- `findFinIdx?_eq_bind_find?_finIdxOf?`: `xs.findFinIdx? p = (xs.find?
p).bind (xs.finIdxOf?)`
- `findIdx_eq_getD_bind_find?_idxOf?`: `xs.findIdx p = ((xs.find?
p).bind (xs.idxOf?)).getD xs.length`

All theorems are provided for `List`, `Array`, and `Vector` (where
applicable).

Requested at
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/show.20that.20Array.2Efind.3F.20and.20Array.2EfindFinIdx.3F.20consistent/near/567340199

🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>
---
 src/Init/Data/Array/Find.lean  | 33 ++++++++++++
 src/Init/Data/List/Find.lean   | 91 +++++++++++++++++++++++++++++++---
 src/Init/Data/Vector/Find.lean | 12 +++++
 3 files changed, 129 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index ca20c6a3f3..e54e9be2f5 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -674,6 +674,39 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
   simp only [Option.map_map, Function.comp_def, Fin.cast_cast]
   simp [Array.size]
 
+/-! ### find? and findFinIdx? -/
+
+theorem find?_eq_map_findFinIdx?_getElem {xs : Array α} {p : α → Bool} :
+    xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
+  cases xs
+  simp [List.find?_eq_map_findFinIdx?_getElem]
+  rfl
+
+theorem find?_eq_bind_findIdx?_getElem? {xs : Array α} {p : α → Bool} :
+    xs.find? p = (xs.findIdx? p).bind (xs[·]?) := by
+  cases xs
+  simp [List.find?_eq_bind_findIdx?_getElem?]
+
+theorem find?_eq_getElem?_findIdx {xs : Array α} {p : α → Bool} :
+    xs.find? p = xs[xs.findIdx p]? := by
+  cases xs
+  simp [List.find?_eq_getElem?_findIdx]
+
+theorem findIdx?_eq_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = (xs.find? p).bind (xs.idxOf? ·) := by
+  cases xs
+  simp [List.findIdx?_eq_bind_find?_idxOf?]
+
+theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
+    xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
+  cases xs
+  simp [List.findFinIdx?_eq_bind_find?_finIdxOf?]
+
+theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
+    xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by
+  cases xs
+  simp [List.findIdx_eq_getD_bind_find?_idxOf?]
+
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index e01b6e2854..1db28dac46 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -1077,6 +1077,37 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
     simp [hf, findFinIdx?_cons]
     split <;> simp [ih, Function.comp_def]
 
+/-! ### find? and findFinIdx? -/
+
+theorem find?_eq_map_findFinIdx?_getElem {xs : List α} {p : α → Bool} :
+    xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [find?_cons, findFinIdx?_cons]
+    split <;> rename_i h
+    · simp [h]
+    · simp [h, ih, Function.comp_def]
+
+theorem find?_eq_bind_findIdx?_getElem? {xs : List α} {p : α → Bool} :
+    xs.find? p = (xs.findIdx? p).bind (xs[·]?) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [find?_cons, findIdx?_cons]
+    split <;> rename_i h
+    · simp [h]
+    · simp [h, ih, Option.bind_map, Function.comp_def]
+
+theorem find?_eq_getElem?_findIdx {xs : List α} {p : α → Bool} :
+    xs.find? p = xs[xs.findIdx p]? := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [find?_cons, findIdx_cons]
+    split <;> rename_i h
+    · simp [h]
+    · simp [h, ih]
 
 /-! ### idxOf
 
@@ -1103,8 +1134,6 @@ theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
   · rw [if_neg]
     simpa using h
 
-
-
 theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.idxOf a = l.length := by
   induction l with
   | nil => rfl
@@ -1113,8 +1142,6 @@ theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.
     simp only [idxOf_cons, cond_eq_ite, beq_iff_eq]
     split <;> simp_all
 
-
-
 theorem idxOf_lt_length_of_mem [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l) : l.idxOf a < l.length := by
   induction l with
   | nil => simp at h
@@ -1143,8 +1170,6 @@ theorem idxOf_lt_length_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
 
 grind_pattern idxOf_lt_length_iff => l.idxOf a, l.length
 
-
-
 /-! ### finIdxOf?
 
 The verification API for `finIdxOf?` is still incomplete.
@@ -1214,7 +1239,9 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
   · rintro w x h rfl
     contradiction
 
-
+theorem idxOf?_eq_some_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} :
+    l.idxOf? a = some i ↔ ∃ (h : i < l.length), l[i] = a ∧ ∀ j (_ : j < i), ¬l[j] = a := by
+  simp [idxOf?, findIdx?_eq_some_iff_getElem]
 
 @[simp, grind =]
 theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
@@ -1230,6 +1257,56 @@ theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.idxOf? a).isNone = ¬ a ∈ l := by
   simp
 
+theorem finIdxOf?_eq_pmap_idxOf? {l : List α} {a : α} [BEq α] [LawfulBEq α] :
+    l.finIdxOf? a =
+      (l.idxOf? a).pmap
+        (fun i h => ⟨i, (idxOf?_eq_some_iff.mp h).1⟩)
+        (fun _ h => h) := by
+  ext ⟨i, h⟩
+  simp only [finIdxOf?_eq_some_iff, Fin.getElem_fin, Fin.forall_iff, Fin.mk_lt_mk,
+    idxOf?_eq_some_iff, Option.pmap_eq_some_iff, Fin.mk.injEq, exists_and_left, exists_prop,
+    and_self_left, exists_eq_right', h, exists_true_left, and_congr_right_iff]
+  intro w
+  constructor
+  · intro w j h₁
+    apply w <;> omega
+  · intro w j h₁ h₂
+    apply w <;> omega
+
+/-! ### find? and idxOf? -/
+
+theorem findIdx?_eq_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.find? p).bind (xs.idxOf?) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp [findIdx?_cons, find?_cons]
+    split <;> rename_i h
+    · simp [h, idxOf?_cons]
+    · simp [h, ih, Function.comp_def, idxOf?_cons]
+      cases w : xs.find? p with
+      | none => simp
+      | some x' =>
+        simp
+        rintro rfl
+        have := find?_some w
+        contradiction
+
+theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool} :
+    xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf?) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_eq_bind_find?_idxOf?, finIdxOf?_eq_pmap_idxOf?]
+  ext i
+  simp only [Option.bind_eq_some_iff, Option.pmap_eq_some_iff, exists_and_left, and_exists_self]
+  constructor
+  · rintro ⟨a, ⟨h₁, h₂⟩, rfl⟩
+    exact ⟨h₁, by simp [h₂]⟩
+  · rintro ⟨h₁, h₂, a, h₃, rfl⟩
+    exact ⟨a, ⟨h₁, h₂, h₃⟩, rfl⟩
+
+theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool} :
+    xs.findIdx p = ((xs.find? p).bind (xs.idxOf?)).getD xs.length := by
+  rw [findIdx_eq_getD_findIdx?, findIdx?_eq_bind_find?_idxOf?]
+
 /-! ### lookup -/
 
 section lookup
diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean
index b059a5a761..aeb211aaec 100644
--- a/src/Init/Data/Vector/Find.lean
+++ b/src/Init/Data/Vector/Find.lean
@@ -341,4 +341,16 @@ theorem isNone_findFinIdx? {xs : Vector α n} {p : α → Bool} :
   rcases xs with ⟨xs, rfl⟩
   simp [hf, Function.comp_def]
 
+/-! ### find? and findFinIdx? -/
+
+theorem find?_eq_map_findFinIdx?_getElem {xs : Vector α n} {p : α → Bool} :
+    xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.find?_eq_map_findFinIdx?_getElem]
+
+theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Vector α n} {p : α → Bool} :
+    xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.findFinIdx?_eq_bind_find?_finIdxOf?]
+
 end Vector