chore: review Array operations argument order (#6041)

This PR modifies the order of arguments for higher-order `Array`
functions, preferring to put the `Array` last (besides positional
arguments with defaults). This is more consistent with the `List` API,
and is more flexible, as dot notation allows two different partially
applied versions.

Author: kim-em

src/Init/Data/Array/Basic.lean

@@ -458,26 +458,26 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
   as.mapFinIdxM fun i a => f i a
 
 @[inline]
-def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
+def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
   for a in as do
     match (← f a) with
     | some b => return b
     | _      => pure ⟨⟩
   return none
 
 @[inline]
-def findM? {α : Type} {m : Type → Type} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) := do
+def findM? {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
       return a
   return none
 
 @[inline]
-def findIdxM? [Monad m] (as : Array α) (p : α → m Bool) : m (Option Nat) := do
+def findIdxM? [Monad m] (p : α → m Bool) (as : Array α) : m (Option Nat) := do
   let mut i := 0
   for a in as do
     if (← p a) then
@@ -529,7 +529,7 @@ def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
   return !(← as.anyM (start := start) (stop := stop) fun v => return !(← p v))
 
 @[inline]
-def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) :=
+def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) :=
   let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
     | 0,   _ => pure none
     | i+1, h => do
@@ -543,7 +543,7 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
   find as.size (Nat.le_refl _)
 
 @[inline]
-def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) :=
+def findRevM? {α : Type} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) :=
   as.findSomeRevM? fun a => return if (← p a) then some a else none
 
 @[inline]
@@ -572,37 +572,37 @@ def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → 
   Id.run <| as.mapFinIdxM f
 
 @[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
 def zipWithIndex (arr : Array α) : Array (α × Nat) :=
   arr.mapIdx fun i a => (a, i)
 
 @[inline]
-def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
+def find? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
   Id.run <| as.findM? p
 
 @[inline]
-def findSome? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
+def findSome? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
   Id.run <| as.findSomeM? f
 
 @[inline]
-def findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α → Option β) : β :=
-  match findSome? a f with
+def findSome! {α : Type u} {β : Type v} [Inhabited β] (f : α → Option β) (a : Array α) : β :=
+  match a.findSome? f with
   | some b => b
   | none   => panic! "failed to find element"
 
 @[inline]
-def findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β :=
+def findSomeRev? {α : Type u} {β : Type v} (f : α → Option β) (as : Array α) : Option β :=
   Id.run <| as.findSomeRevM? f
 
 @[inline]
-def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
+def findRev? {α : Type} (p : α → Bool) (as : Array α) : Option α :=
   Id.run <| as.findRevM? p
 
 @[inline]
-def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
+def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (j : Nat) :=
     if h : j < as.size then

src/Init/Data/Array/Lemmas.lean

@@ -210,7 +210,7 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 
 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
+    findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by
   induction i generalizing l with
   | zero => simp [Array.findSomeRevM?.find.eq_def]
   | succ i ih =>
@@ -1470,7 +1470,7 @@ termination_by stop - start
 
 -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
-    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+    as.any p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
   dsimp [any, anyM, Id.run]
   split
   · rw [anyM_loop_iff_exists]; rfl
@@ -1482,7 +1482,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
       exact ⟨i, by omega, by omega, h⟩
 
 theorem any_eq_true {p : α → Bool} {as : Array α} :
-    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+    as.any p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
 
 theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
@@ -1502,20 +1502,20 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
   rw [List.allM_eq_not_anyM_not]
 
 theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
-    all as p start stop = !(any as (!p ·) start stop) := by
+    as.all p start stop = !(as.any (!p ·) start stop) := by
   dsimp [all, allM]
   rfl
 
 theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
-    all as p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
+    as.all p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
   rw [all_eq_not_any_not]
-  suffices ¬(any as (!p ·) start stop = true) ↔
+  suffices ¬(as.any (!p ·) start stop = true) ↔
       ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
     simp_all
   rw [any_iff_exists]
   simp
 
-theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
+theorem all_eq_true {p : α → Bool} {as : Array α} : as.all p ↔ ∀ i : Fin as.size, p as[i] := by
   simp [all_iff_forall, Fin.isLt]
 
 theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by

src/Init/Data/Array/MapIdx.lean

@@ -66,35 +66,35 @@ theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
 
 /-! ### mapIdx -/
 
-theorem mapIdx_induction (as : Array α) (f : Nat → α → β)
+theorem mapIdx_induction (f : Nat → α → β) (as : Array α)
     (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+    motive as.size ∧ ∃ eq : (as.mapIdx f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
   mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
 
-theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
+theorem mapIdx_spec (f : Nat → α → β) (as : Array α)
     (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
-    ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+    ∃ eq : (as.mapIdx f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
   (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
 
-@[simp] theorem size_mapIdx (a : Array α) (f : Nat → α → β) : (a.mapIdx f).size = a.size :=
+@[simp] theorem size_mapIdx (f : Nat → α → β) (as : Array α) : (as.mapIdx f).size = as.size :=
   (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
 
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat)
-    (h : i < (mapIdx a f).size) :
-    (a.mapIdx f)[i] = f i (a[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i (by simp_all)
+@[simp] theorem getElem_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat)
+    (h : i < (as.mapIdx f).size) :
+    (as.mapIdx f)[i] = f i (as[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i as[i]) fun _ => rfl).2 i (by simp_all)
 
-@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat) :
-    (a.mapIdx f)[i]? =
-      a[i]?.map (f i) := by
+@[simp] theorem getElem?_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) :
+    (as.mapIdx f)[i]? =
+      as[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
-@[simp] theorem toList_mapIdx (a : Array α) (f : Nat → α → β) :
-    (a.mapIdx f).toList = a.toList.mapIdx (fun i a => f i a) := by
+@[simp] theorem toList_mapIdx (f : Nat → α → β) (as : Array α) :
+    (as.mapIdx f).toList = as.toList.mapIdx (fun i a => f i a) := by
   apply List.ext_getElem <;> simp
 
 end Array
@@ -105,7 +105,7 @@ namespace List
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 
-@[simp] theorem mapIdx_toArray (l : List α) (f : Nat → α → β) :
+@[simp] theorem mapIdx_toArray (f : Nat → α → β) (l : List α) :
     l.toArray.mapIdx f = (l.mapIdx f).toArray := by
   ext <;> simp