feat: theorems about == on Vector (#6376)

This PR adds theorems about `==` on `Vector`, reproducing those already
on `List` and `Array`.

src/Init/Data/Array/Find.lean

@@ -99,7 +99,7 @@ theorem back?_flatten {L : Array (Array α)} :
   simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
 
 theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
-  simp [mkArray_eq_toArray_replicate, List.findSome?_replicate]
+  simp [← List.toArray_replicate, List.findSome?_replicate]
 
 @[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
   simp [findSome?_mkArray, Nat.ne_of_gt h]
@@ -246,7 +246,7 @@ theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β →
 
 theorem find?_mkArray :
     find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
-  simp [mkArray_eq_toArray_replicate, List.find?_replicate]
+  simp [← List.toArray_replicate, List.find?_replicate]
 
 @[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
     find? p (mkArray n a) = if p a then some a else none := by
@@ -262,15 +262,15 @@ theorem find?_mkArray :
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
     (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
-  simp [mkArray_eq_toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
+  simp [← List.toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
 
 @[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} :
     (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
-  simp [mkArray_eq_toArray_replicate]
+  simp [← List.toArray_replicate]
 
 @[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
     ((mkArray n a).find? p).get h = a := by
-  simp [mkArray_eq_toArray_replicate]
+  simp [← List.toArray_replicate]
 
 theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
     (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :

src/Init/Data/Array/Lemmas.lean

@@ -25,8 +25,8 @@ namespace Array
 
 /-! ### toList -/
 
-theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
-  cases a; cases b; simpa using h
+theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b := by
+  cases a; cases b; simp
 
 @[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[] := by
   cases l <;> simp
@@ -143,6 +143,34 @@ theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
     ∃ (ys : Array α) (a : α), xs = ys.push a :=
   exists_push_of_size_pos (by simp [h])
 
+theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+  simp
+
+/-! ### mkArray -/
+
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
+@[simp] theorem toList_mkArray : (mkArray n a).toList = List.replicate n a := by
+  simp only [mkArray]
+
+@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl
+
+theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by
+  apply toList_inj.1
+  simp [List.replicate_succ']
+
+theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
+  rw [← List.replicate_inj, ← toList_inj]
+  simp
+
+@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
+    (mkArray n v)[i] = v := by simp [← getElem_toList]
+
+theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
+    (mkArray n v)[i]? = if i < n then some v else none := by
+  simp [getElem?_def]
+
 /-! ## L[i] and L[i]? -/
 
 @[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
@@ -894,11 +922,60 @@ theorem mem_or_eq_of_mem_setIfInBounds
   · simp
   · simp [List.set_eq_of_length_le (by simpa using h)]
 
-/-! Content below this point has not yet been aligned with `List`. -/
+/-! ### BEq -/
 
-theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+@[simp] theorem push_beq_push [BEq α] {a b : α} {v : Array α} {w : Array α} :
+    (v.push a == w.push b) = (v == w && a == b) := by
+  cases v
+  cases w
   simp
 
+@[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
+    (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]
+    rw [Bool.eq_iff_iff]
+    simp +contextual
+
+@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
+  constructor
+  · intro h
+    constructor
+    intro a
+    suffices (#[a] == #[a]) = true by
+      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+    simp
+  · intro h
+    constructor
+    apply Array.isEqv_self_beq
+
+@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α := by
+  constructor
+  · intro h
+    constructor
+    · intro a b h
+      apply singleton_inj.1
+      apply eq_of_beq
+      simp only [instBEq, isEqv, isEqvAux]
+      simpa
+    · intro a
+      suffices (#[a] == #[a]) = true by
+        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+      simp
+  · intro h
+    constructor
+    · intro a b h
+      obtain ⟨hs, hi⟩ := rel_of_isEqv h
+      ext i h₁ h₂
+      · exact hs
+      · simpa using hi _ h₁
+    · intro a
+      apply Array.isEqv_self_beq
+
+/-! Content below this point has not yet been aligned with `List`. -/
+
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
 
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
@@ -1083,22 +1160,6 @@ theorem ofFn_succ (f : Fin (n+1) → α) :
       simp at h₁ h₂
       omega
 
-/-! # mkArray -/
-
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
-@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
-
-theorem mkArray_eq_toArray_replicate (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray := rfl
-
-@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [← getElem_toList]
-
-theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
-    (mkArray n v)[i]? = if i < n then some v else none := by
-  simp [getElem?_def]
-
 /-! # mem -/
 
 @[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
@@ -1310,43 +1371,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
-/-! ### BEq -/
-
-@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
-  constructor
-  · intro h
-    constructor
-    intro a
-    suffices (#[a] == #[a]) = true by
-      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
-    simp
-  · intro h
-    constructor
-    apply Array.isEqv_self_beq
-
-@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α := by
-  constructor
-  · intro h
-    constructor
-    · intro a b h
-      apply singleton_inj.1
-      apply eq_of_beq
-      simp only [instBEq, isEqv, isEqvAux]
-      simpa
-    · intro a
-      suffices (#[a] == #[a]) = true by
-        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
-      simp
-  · intro h
-    constructor
-    · intro a b h
-      obtain ⟨hs, hi⟩ := rel_of_isEqv h
-      ext i h₁ h₂
-      · exact hs
-      · simpa using hi _ h₁
-    · intro a
-      apply Array.isEqv_self_beq
-
 /-! ### take -/
 
 @[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by

src/Init/Data/List/Lemmas.lean

@@ -154,6 +154,9 @@ theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b L, l = b :: L
 theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
   simp
 
+@[simp] theorem concat_ne_nil (a : α) (l : List α) : l ++ [a] ≠ [] := by
+  cases l <;> simp
+
 /-! ## L[i] and L[i]? -/
 
 /-! ### `get` and `get?`.
@@ -717,6 +720,15 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
 @[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
     (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
 
+@[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
+    (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b) := by
+  induction l₁ generalizing l₂ with
+  | nil => cases l₂ <;> simp
+  | cons x l₁ ih =>
+    cases l₂ with
+    | nil => simp
+    | cons y l₂ => simp [ih, Bool.and_assoc]
+
 theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
   match l₁, l₂ with
   | [], [] => rfl
@@ -2074,8 +2086,6 @@ theorem concat_inj_right {l : List α} {a a' : α} : concat l a = concat l a' 
 
 @[deprecated concat_inj (since := "2024-09-05")] abbrev concat_eq_concat := @concat_inj
 
-theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by cases l <;> simp
-
 theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
 
 theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
@@ -2328,6 +2338,10 @@ theorem flatMap_eq_foldl (f : α → List β) (l : List α) :
 
 @[simp] theorem replicate_one : replicate 1 a = [a] := rfl
 
+/-- Variant of `replicate_succ` that concatenates `a` to the end of the list. -/
+theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a] := by
+  induction n <;> simp_all [replicate_succ, ← cons_append]
+
 @[simp] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
   | 0 => by simp
   | n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]

src/Init/Data/List/ToArray.lean

@@ -371,4 +371,9 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
   · simp
   · simp_all [List.set_eq_of_length_le]
 
+@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
+
+@[deprecated toArray_replicate (since := "2024-12-13")]
+abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
+
 end List