feat: add List.findRev? and findSomeRev?, and simp lemmas

src/Init/Data/List/Basic.lean

@@ -1655,6 +1655,42 @@ theorem findSome?_cons {f : α → Option β} :
     (a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f :=
   rfl
 
+/-! ### findRev? -/
+
+/--
+Returns the last element of the list for which the predicate `p` returns `true`, or `none` if no
+such element is found.
+
+`O(|l|)`.
+
+Examples:
+* `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 2`
+* `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
+-/
+def findRev? (p : α → Bool) : List α → Option α
+  | []    => none
+  | a::as => match findRev? p as with
+    | some b => some b
+    | none   => if p a then some a else none
+
+/-! ### findSomeRev? -/
+
+/--
+Returns the last non-`none` result of applying `f` to each element of the list in order. Returns
+`none` if `f` returns `none` for all elements of the list.
+
+`O(|l|)`.
+
+Examples:
+ * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 5 then some (10 * x) else none) = some 20`
+ * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 1 then some (10 * x) else none) = none`
+-/
+def findSomeRev? (f : α → Option β) : List α → Option β
+  | []    => none
+  | a::as => match findSomeRev? f as with
+    | some b => some b
+    | none   => f a
+
 /-! ### findIdx -/
 
 /--

src/Init/Data/List/Find.lean

@@ -8,6 +8,7 @@ prelude
 import Init.Data.List.Lemmas
 import Init.Data.List.Sublist
 import Init.Data.List.Range
+import Init.Data.List.Impl
 import Init.Data.Fin.Lemmas
 
 /-!
@@ -25,10 +26,6 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp] theorem findSome?_singleton {a : α} {f : α → Option β} : [a].findSome? f = f a := by
-  simp only [findSome?]
-  split <;> simp_all
-
 @[simp] theorem findSome?_cons_of_isSome {l} (h : (f a).isSome) : findSome? f (a :: l) = f a := by
   simp only [findSome?]
   split <;> simp_all
@@ -138,13 +135,6 @@ theorem findSome?_map {f : β → γ} {l : List β} : findSome? p (l.map f) = l.
     simp only [map_cons, findSome?]
     split <;> simp_all
 
-theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
-  induction l₁ with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [cons_append, findSome?]
-    split <;> simp_all
-
 theorem head_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
     (flatten L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
   simp [head_eq_iff_head?_eq_some, head?_flatten]
@@ -206,10 +196,6 @@ theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (
 
 /-! ### find? -/
 
-@[simp] theorem find?_singleton {a : α} {p : α → Bool} : [a].find? p = if p a then some a else none := by
-  simp only [find?]
-  split <;> simp_all
-
 @[simp] theorem find?_cons_of_pos {l} (h : p a) : find? p (a :: l) = some a := by
   simp [find?, h]
 
@@ -336,13 +322,6 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
     simp only [map_cons, find?]
     by_cases h : p (f x) <;> simp [h, ih]
 
-@[simp] theorem find?_append {l₁ l₂ : List α} : (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
-  induction l₁ with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [cons_append, find?]
-    by_cases h : p x <;> simp [h, ih]
-
 @[simp] theorem find?_flatten {xss : List (List α)} {p : α → Bool} :
     xss.flatten.find? p = xss.findSome? (·.find? p) := by
   induction xss with

src/Init/Data/List/Impl.lean

@@ -17,8 +17,7 @@ then at runtime you will get non-tail recursive versions of the following defini
 -/
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- TODO: restore after an update-stage0
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -255,6 +254,62 @@ Examples:
 @[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
   funext α l; simp [dropLastTR]
 
+/-! ## Finding elements -/
+
+/-- Tail recursive implementation of `findRev?`. This is only used at runtime. -/
+def findRev?TR (p : α → Bool) (l : List α) : Option α := l.reverse.find? p
+
+@[simp] theorem find?_singleton {a : α} : [a].find? p = if p a then some a else none := by
+  simp only [find?]
+  split <;> simp_all
+
+@[simp] theorem find?_append {xs ys : List α} : (xs ++ ys).find? p = (xs.find? p).or (ys.find? p) := by
+  induction xs with
+  | nil => simp [find?]
+  | cons x xs ih =>
+    simp only [cons_append, find?_cons, ih]
+    split <;> simp
+
+@[csimp] theorem findRev?_eq_findRev?TR : @List.findRev? = @List.findRev?TR := by
+  apply funext; intro α; apply funext; intro p; apply funext; intro l
+  induction l with
+  | nil => simp [findRev?, findRev?TR]
+  | cons x l ih =>
+    simp only [findRev?, ih, findRev?TR, reverse_cons, find?_append, find?_singleton]
+    split <;> simp_all
+
+@[simp] theorem findRev?_eq_find?_reverse {l : List α} {p : α → Bool} :
+    l.findRev? p = l.reverse.find? p := by
+  simp [findRev?_eq_findRev?TR, findRev?TR]
+
+/-- Tail recursive implementation of `finSomedRev?`. This is only used at runtime. -/
+def findSomeRev?TR (f : α → Option β) (l : List α) : Option β := l.reverse.findSome? f
+
+@[simp] theorem findSome?_singleton {a : α} :
+    [a].findSome? f = f a := by
+  simp only [findSome?_cons, findSome?_nil]
+  split <;> simp_all
+
+@[simp] theorem findSome?_append {xs ys : List α} : (xs ++ ys).findSome? f = (xs.findSome? f).or (ys.findSome? f) := by
+  induction xs with
+  | nil => simp [findSome?]
+  | cons x xs ih =>
+    simp only [cons_append, findSome?_cons, ih]
+    split <;> simp
+
+@[csimp] theorem findSomeRev?_eq_findSomeRev?TR : @List.findSomeRev? = @List.findSomeRev?TR := by
+  apply funext; intro α; apply funext; intro β; apply funext; intro p; apply funext; intro l
+  induction l with
+  | nil => simp [findSomeRev?, findSomeRev?TR]
+  | cons x l ih =>
+    simp only [findSomeRev?, ih, findSomeRev?TR, reverse_cons, findSome?_append,
+      findSome?_singleton]
+    split <;> simp_all
+
+@[simp] theorem findSomeRev?_eq_findSome?_reverse {l : List α} {f : α → Option β} :
+    l.findSomeRev? f = l.reverse.findSome? f := by
+  simp [findSomeRev?_eq_findSomeRev?TR, findSomeRev?TR]
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/