feat: align List/Array/Vector.reverse lemmas

src/Init/Data/Array/Lemmas.lean

@@ -2269,7 +2269,7 @@ theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (
   rw [← toList_inj]
   simp [flatMap_toList, List.flatMap_replicate]
 
-@[simp] theorem isEmpty_replicate : (mkArray n a).isEmpty = decide (n = 0) := by
+@[simp] theorem isEmpty_mkArray : (mkArray n a).isEmpty = decide (n = 0) := by
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
@@ -2277,6 +2277,168 @@ theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (
   rw [← List.toArray_replicate, List.sum_toArray]
   simp
 
+/-! ### Preliminaries about `swap` needed for `reverse`. -/
+
+theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
+    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
+  simp [swap]
+
+theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
+    if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
+  simp [swap_def, getElem?_set]
+
+/-! ### reverse -/
+
+@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
+  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
+    rw [reverse.loop]
+    if h : i < j then
+      simp [(go · (i+1) ⟨j-1, ·⟩), h]
+    else simp [h]
+    termination_by j - i
+  simp only [reverse]; split <;> simp [go]
+
+@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
+  let rec go (as : Array α) (i j hj)
+      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
+      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
+      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
+    rw [reverse.loop]; dsimp only; split <;> rename_i h₁
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
+      rw [(go · (i+1) j)]
+      · rwa [Nat.add_right_comm i]
+      · simp [size_swap, h₂]
+      · intro k
+        rw [getElem?_toList, getElem?_swap]
+        simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
+          ← getElem?_toList]
+        split <;> rename_i h₂
+        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+        split <;> rename_i h₃
+        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
+          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+    · rw [H]; split <;> rename_i h₂
+      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
+        cases Nat.le_antisymm h₂.1 h₂.2
+        exact (List.getElem?_reverse' _ _ h).symm
+      · rfl
+    termination_by j - i
+  simp only [reverse]
+  split
+  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
+  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
+    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    split
+    · rfl
+    · rename_i h
+      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
+        true_and, Nat.not_lt] at h
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
+
+@[simp] theorem _root_.List.reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
+  apply ext'
+  simp only [toList_reverse]
+
+@[simp] theorem reverse_push (as : Array α) (a : α) : (as.push a).reverse = #[a] ++ as.reverse := by
+  cases as
+  simp
+
+@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
+  cases as
+  simp
+
+@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
+    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by
+  cases as
+  simp
+
+@[simp] theorem reverse_eq_empty_iff {xs : Array α} : xs.reverse = #[] ↔ xs = #[] := by
+  cases xs
+  simp
+
+theorem reverse_ne_empty_iff {xs : Array α} : xs.reverse ≠ #[] ↔ xs ≠ #[] :=
+  not_congr reverse_eq_empty_iff
+
+/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
+theorem getElem?_reverse' {l : Array α} (i j) (h : i + j + 1 = l.size) : l.reverse[i]? = l[j]? := by
+  rcases l with ⟨l⟩
+  simp at h
+  simp only [List.reverse_toArray, List.getElem?_toArray]
+  rw [List.getElem?_reverse' (l := l) _ _ h]
+
+@[simp]
+theorem getElem?_reverse {l : Array α} {i} (h : i < l.size) :
+    l.reverse[i]? = l[l.size - 1 - i]? := by
+  cases l
+  simp_all
+
+@[simp] theorem reverse_reverse (as : Array α) : as.reverse.reverse = as := by
+  cases as
+  simp
+
+theorem reverse_eq_iff {as bs : Array α} : as.reverse = bs ↔ as = bs.reverse := by
+  constructor <;> (rintro rfl; simp)
+
+@[simp] theorem reverse_inj {xs ys : Array α} : xs.reverse = ys.reverse ↔ xs = ys := by
+  simp [reverse_eq_iff]
+
+@[simp] theorem reverse_eq_push_iff {xs : Array α} {ys : Array α} {a : α} :
+    xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse := by
+  rw [reverse_eq_iff, reverse_push]
+
+@[simp] theorem map_reverse (f : α → β) (l : Array α) : l.reverse.map f = (l.map f).reverse := by
+  cases l <;> simp [*]
+
+@[simp] theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
+  cases l
+  simp
+
+@[simp] theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
+  cases l
+  simp
+
+@[simp] theorem reverse_append (as bs : Array α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+  cases as
+  cases bs
+  simp
+
+@[simp] theorem reverse_eq_append_iff {xs ys zs : Array α} :
+    xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
+  cases xs
+  cases ys
+  cases zs
+  simp
+
+/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
+theorem reverse_flatten (L : Array (Array α)) :
+    L.flatten.reverse = (L.map reverse).reverse.flatten := by
+  cases L using array₂_induction
+  simp [flatten_toArray, List.reverse_flatten, Function.comp_def]
+
+/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
+theorem flatten_reverse (L : Array (Array α)) :
+    L.reverse.flatten = (L.map reverse).flatten.reverse := by
+  cases L using array₂_induction
+  simp [flatten_toArray, List.flatten_reverse, Function.comp_def]
+
+theorem reverse_flatMap {β} (l : Array α) (f : α → Array β) :
+    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
+  cases l
+  simp [List.reverse_flatMap, Function.comp_def]
+
+theorem flatMap_reverse {β} (l : Array α) (f : α → Array β) :
+    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
+  cases l
+  simp [List.flatMap_reverse, Function.comp_def]
+
+@[simp] theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a := by
+  rw [← toList_inj]
+  simp
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/
@@ -2468,6 +2630,7 @@ theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
+@[deprecated getElem_set_self (since := "2025-01-17")]
 theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, ← getElem_toList, List.getElem_set_self]
@@ -2491,17 +2654,9 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
-theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
-    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
-  simp [swap]
-
 @[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) :
     (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
 
-theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
-    if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
-  simp [swap_def, get?_set]
-
 @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) :
     a.swapAt i v hi = (a[i], a.set i v) := rfl
 
@@ -2555,15 +2710,6 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 
 @[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
 
-@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
-  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
-    rw [reverse.loop]
-    if h : i < j then
-      simp [(go · (i+1) ⟨j-1, ·⟩), h]
-    else simp [h]
-    termination_by j - i
-  simp only [reverse]; split <;> simp [go]
-
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
   induction n <;> simp [range]
 
@@ -2574,61 +2720,6 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [← getElem_toList]
 
-@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
-  let rec go (as : Array α) (i j hj)
-      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
-      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
-    rw [reverse.loop]; dsimp only; split <;> rename_i h₁
-    · match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel]
-      rw [(go · (i+1) j)]
-      · rwa [Nat.add_right_comm i]
-      · simp [size_swap, h₂]
-      · intro k
-        rw [getElem?_toList, getElem?_swap]
-        simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          ← getElem?_toList]
-        split <;> rename_i h₂
-        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
-        split <;> rename_i h₃
-        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
-        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
-          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
-    · rw [H]; split <;> rename_i h₂
-      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
-        cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.getElem?_reverse' _ _ h).symm
-      · rfl
-    termination_by j - i
-  simp only [reverse]
-  split
-  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
-  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
-    split
-    · rfl
-    · rename_i h
-      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
-        true_and, Nat.not_lt] at h
-      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
-
-end Array
-
-open Array
-
-namespace List
-
-@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
-  apply ext'
-  simp only [toList_reverse]
-
-end List
-
-namespace Array
-
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) :
@@ -3324,17 +3415,6 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   | nil => simp
   | cons xs xss ih => simp [ih]
 
-/-! ### reverse -/
-
-@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
-  cases as
-  simp
-
-@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
-    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by
-  cases as
-  simp [Array.getElem_reverse]
-
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse

src/Init/Data/Vector/Lemmas.lean

@@ -1746,6 +1746,92 @@ theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f
 @[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkVector n a).sum = n * a := by
   simp [toArray_mkVector]
 
+/-! ### reverse -/
+
+@[simp] theorem reverse_push (as : Vector α n) (a : α) :
+    (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.reverse_push]
+
+@[simp] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
+  cases as
+  simp
+
+@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
+    (a.reverse)[i] = a[n - 1 - i] := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
+/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
+theorem getElem?_reverse' {l : Vector α n} (i j) (h : i + j + 1 = n) : l.reverse[i]? = l[j]? := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.getElem?_reverse' i j h
+
+@[simp]
+theorem getElem?_reverse {l : Vector α n} {i} (h : i < n) :
+    l.reverse[i]? = l[n - 1 - i]? := by
+  cases l
+  simp_all
+
+@[simp] theorem reverse_reverse (as : Vector α n) : as.reverse.reverse = as := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.reverse_reverse]
+
+theorem reverse_eq_iff {as bs : Vector α n} : as.reverse = bs ↔ as = bs.reverse := by
+  constructor <;> (rintro rfl; simp)
+
+@[simp] theorem reverse_inj {xs ys : Vector α n} : xs.reverse = ys.reverse ↔ xs = ys := by
+  simp [reverse_eq_iff]
+
+@[simp] theorem reverse_eq_push_iff {xs : Vector α (n + 1)} {ys : Vector α n} {a : α} :
+    xs.reverse = ys.push a ↔ xs = (#v[a] ++ ys.reverse).cast (by omega) := by
+  rcases xs with ⟨xs, h⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.reverse_eq_push_iff]
+
+@[simp] theorem map_reverse (f : α → β) (l : Vector α n) : l.reverse.map f = (l.map f).reverse := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.map_reverse]
+
+@[simp] theorem reverse_append (as : Vector α n) (bs : Vector α m) :
+    (as ++ bs).reverse = (bs.reverse ++ as.reverse).cast (by omega) := by
+  rcases as with ⟨as, rfl⟩
+  rcases bs with ⟨bs, rfl⟩
+  simp [Array.reverse_append]
+
+@[simp] theorem reverse_eq_append_iff {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} :
+    xs.reverse = ys ++ zs ↔ xs = (zs.reverse ++ ys.reverse).cast (by omega) := by
+  cases xs
+  cases ys
+  cases zs
+  simp
+
+/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
+theorem reverse_flatten (L : Vector (Vector α m) n) :
+    L.flatten.reverse = (L.map reverse).reverse.flatten := by
+  cases L using vector₂_induction
+  simp [Array.reverse_flatten]
+
+/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
+theorem flatten_reverse (L : Vector (Vector α m) n) :
+    L.reverse.flatten = (L.map reverse).flatten.reverse := by
+  cases L using vector₂_induction
+  simp [Array.flatten_reverse]
+
+theorem reverse_flatMap {β} (l : Vector α n) (f : α → Vector β m) :
+    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.reverse_flatMap, Function.comp_def]
+
+theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) :
+    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.flatMap_reverse, Function.comp_def]
+
+@[simp] theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a := by
+  rw [← toArray_inj]
+  simp
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
@@ -1877,13 +1963,6 @@ theorem swap_comm (a : Vector α n) {i j : Nat} {hi hj} :
   cases a
   simp
 
-/-! ### reverse -/
-
-@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
-    (a.reverse)[i] = a[n - 1 - i] := by
-  rcases a with ⟨a, rfl⟩
-  simp
-
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

tests/lean/run/grind_offset.lean

@@ -23,7 +23,7 @@ info: [grind.assert] f (y + 1) = a
 [grind.assert] f (y + 1) = g (f y)
 -/
 #guard_msgs (info) in
-example : f (y + 1) = a → a = g (f y):= by
+example : f (y + 1) = a → a = g (f y) := by
   grind
 
 /--