feat: lemmas relating Array.findX and List.findX (#5985)

This PR relates the operations `findSomeM?`, `findM?`, `findSome?`, and
`find?` on `Array` with the corresponding operations on `List`, and also
provides simp lemmas for the `Array` operations `findSomeRevM?`,
`findRevM?`, `findSomeRev?`, `findRev?` (in terms of `reverse` and the
usual forward find operations).

src/Init/Data/Array/Lemmas.lean

@@ -197,6 +197,58 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
+@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeM? f = l.findSomeM? f := by
+  rw [Array.findSomeM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
+    (i : Nat) (h) :
+    findSomeRevM?.find l.toArray f i h = (l.take i).reverse.findSomeM? f := by
+  induction i generalizing l with
+  | zero => simp [Array.findSomeRevM?.find.eq_def]
+  | succ i ih =>
+    rw [size_toArray] at h
+    rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
+    simp only [ih, reverse_append]
+    congr
+    ext1 (_|_) <;> simp
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`.
+theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by
+  simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`.
+theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findRevM? f = l.reverse.findM? f := by
+  rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]
+
+@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findM? f = l.findM? f := by
+  rw [Array.findM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
+    l.toArray.findSome? f = l.findSome? f := by
+  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
+
+@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
+    l.toArray.find? f = l.find? f := by
+  rw [Array.find?, ← findM?_id, findM?_toArray, Id.run]
+
 theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
     Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
       Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
@@ -1569,6 +1621,28 @@ theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
     (Array.zip as bs).toList = List.zip as.toList bs.toList := by
   simp [zip, toList_zipWith, List.zip]
 
+/-! ### findSomeM?, findM?, findSome?, find? -/
+
+@[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] (p : α → m (Option β)) (as : Array α) :
+    as.toList.findSomeM? p = as.findSomeM? p := by
+  cases as
+  simp
+
+@[simp] theorem findM?_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    as.toList.findM? p = as.findM? p := by
+  cases as
+  simp
+
+@[simp] theorem findSome?_toList (p : α → Option β) (as : Array α) :
+    as.toList.findSome? p = as.findSome? p := by
+  cases as
+  simp
+
+@[simp] theorem find?_toList (p : α → Bool) (as : Array α) :
+    as.toList.find? p = as.find? p := by
+  cases as
+  simp
+
 end Array
 
 open Array
@@ -1805,6 +1879,32 @@ namespace Array
   induction as
   simp
 
+/-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
+
+@[simp] theorem findSomeRevM?_eq_findSomeM?_reverse
+    [Monad m] [LawfulMonad m] (f : α → m (Option β)) (as : Array α) :
+    as.findSomeRevM? f = as.reverse.findSomeM? f := by
+  cases as
+  rw [List.findSomeRevM?_toArray]
+  simp
+
+@[simp] theorem findRevM?_eq_findM?_reverse
+    [Monad m] [LawfulMonad m] (f : α → m Bool) (as : Array α) :
+    as.findRevM? f = as.reverse.findM? f := by
+  cases as
+  rw [List.findRevM?_toArray]
+  simp
+
+@[simp] theorem findSomeRev?_eq_findSome?_reverse (f : α → Option β) (as : Array α) :
+    as.findSomeRev? f = as.reverse.findSome? f := by
+  cases as
+  simp [findSomeRev?, Id.run]
+
+@[simp] theorem findRev?_eq_find?_reverse (f : α → Bool) (as : Array α) :
+    as.findRev? f = as.reverse.find? f := by
+  cases as
+  simp [findRev?, Id.run]
+
 /-! ### unzip -/
 
 @[simp] theorem fst_unzip (as : Array (α × β)) : (Array.unzip as).fst = as.map Prod.fst := by

src/Init/Data/List/Control.lean

@@ -5,6 +5,8 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Control.Basic
+import Init.Control.Id
+import Init.Control.Lawful
 import Init.Data.List.Basic
 
 namespace List
@@ -207,6 +209,16 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
     | true  => pure (some a)
     | false => findM? p as
 
+@[simp]
+theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [findM?, find?]
+    cases p a with
+    | true  => rfl
+    | false => rw [ih]; rfl
+
 @[specialize]
 def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
   | []    => pure none
@@ -215,6 +227,28 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | some b => pure (some b)
     | none   => findSomeM? f as
 
+@[simp]
+theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [findSomeM?, findSome?]
+    cases f a with
+    | some b => rfl
+    | none   => rw [ih]; rfl
+
+theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
+    as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [findM?, findSomeM?]
+    simp [ih]
+    congr
+    apply funext
+    intro b
+    cases b <;> simp
+
 @[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b