feat: theorems about == on Vector

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
@@ -1088,22 +1165,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
@@ -1315,43 +1376,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?`.
@@ -715,6 +718,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
@@ -2072,8 +2084,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
@@ -2326,6 +2336,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

src/Init/Data/Vector/Lemmas.lean

@@ -22,6 +22,7 @@ end Array
 
 namespace Vector
 
+
 /-! ### mk lemmas -/
 
 theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
@@ -49,6 +50,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem pop_mk {data : Array α} {size : data.size = n} :
     (Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl
 
+@[simp] theorem mk_beq_mk [BEq α] {a b : Array α} {h : a.size = n} {h' : b.size = n} :
+    (Vector.mk a h == Vector.mk b h') = (a == b) := by
+  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, h, h']
+
 @[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
     (Vector.mk a h).allDiff = a.allDiff := rfl
 
@@ -181,6 +186,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 
 @[simp] theorem toArray_push (a : Vector α n) (x) : (a.push x).toArray = a.toArray.push x := rfl
 
+@[simp] theorem toArray_beq_toArray [BEq α] (a : Vector α n) (b : Vector α n) :
+    (a.toArray == b.toArray) = (a == b) := by
+  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]
+
 @[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
 
 @[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl
@@ -236,8 +245,25 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
   cases v
   simp
 
-theorem toArray_inj : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w
-  | {..}, {..}, rfl => rfl
+@[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
+
+theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by
+  cases v
+  cases w
+  simp
+
+/--
+`Vector.ext` is an extensionality theorem.
+Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
+-/
+@[ext]
+protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
+  apply Vector.toArray_inj.1
+  apply Array.ext
+  · rw [a.size_toArray, b.size_toArray]
+  · intro i hi _
+    rw [a.size_toArray] at hi
+    exact h i hi
 
 @[simp] theorem toArray_eq_empty_iff (v : Vector α n) : v.toArray = #[] ↔ n = 0 := by
   rcases v with ⟨v, h⟩
@@ -293,6 +319,10 @@ theorem toList_pop (a : Vector α n) : a.pop.toList = a.toList.dropLast := rfl
 
 theorem toList_push (a : Vector α n) (x) : (a.push x).toList = a.toList ++ [x] := by simp
 
+@[simp] theorem toList_beq_toList [BEq α] (a : Vector α n) (b : Vector α n) :
+    (a.toList == b.toList) = (a == b) := by
+  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]
+
 theorem toList_range : (Vector.range n).toList = List.range n := by simp
 
 theorem toList_reverse (a : Vector α n) : a.reverse.toList = a.toList.reverse := by simp
@@ -335,8 +365,12 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) :
   cases v
   simp
 
-theorem toList_inj : ∀ {v w : Vector α n}, v.toList = w.toList → v = w
-  | {..}, {..}, rfl => rfl
+@[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl
+
+theorem toList_inj {v w : Vector α n} : v.toList = w.toList ↔ v = w := by
+  cases v
+  cases w
+  simp [Array.toList_inj]
 
 @[simp] theorem toList_eq_empty_iff (v : Vector α n) : v.toList = [] ↔ n = 0 := by
   rcases v with ⟨v, h⟩
@@ -356,7 +390,7 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim
 
 /-- A vector of length `0` is the empty vector. -/
 protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
-  apply Vector.toArray_inj
+  apply Vector.toArray_inj.1
   apply Array.eq_empty_of_size_eq_zero v.2
 
 
@@ -364,7 +398,7 @@ protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
 
 theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm := by
   rcases xs with ⟨xs, rfl⟩
-  apply toArray_inj
+  apply toArray_inj.1
   simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h
   simp [h]
 
@@ -405,7 +439,20 @@ theorem exists_push {xs : Vector α (n + 1)} :
     ∃ (ys : Vector α n) (a : α), xs = ys.push a := by
   rcases xs with ⟨xs, w⟩
   obtain ⟨ys, a, h⟩ := Array.exists_push_of_size_eq_add_one w
-  exact ⟨⟨ys, by simp_all⟩, a, toArray_inj h⟩
+  exact ⟨⟨ys, by simp_all⟩, a, toArray_inj.1 h⟩
+
+theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
+  simp
+
+/-! ### mkVector -/
+
+@[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl
+
+theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by
+  simp [mkVector, Array.mkArray_succ]
+
+theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by
+  simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj]
 
 /-! ## L[i] and L[i]? -/
 
@@ -908,6 +955,67 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   simp [mem_iff_getElem]
   exact ⟨i, (by simpa using hi), by simp⟩
 
+/-! ### BEq -/
+
+@[simp] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {v : Vector α n} {w : Vector α n} :
+    (v.push a == w.push b) = (v == w && a == b) := by
+  cases v
+  cases w
+  simp
+
+@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
+    (mkVector n a == mkVector n b) = (n == 0 || a == b) := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]
+    rw [Bool.eq_iff_iff]
+    simp +contextual
+
+@[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ↔ ReflBEq α := by
+  match n, NeZero.ne n with
+  | n + 1, _ =>
+    constructor
+    · intro h
+      constructor
+      intro a
+      suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
+        rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
+        exact this.2
+      simp
+    · intro h
+      constructor
+      rintro ⟨v, h⟩
+      simpa using Array.isEqv_self_beq ..
+
+@[simp] theorem lawfulBEq_iff [BEq α] [NeZero n] : LawfulBEq (Vector α n) ↔ LawfulBEq α := by
+  match n, NeZero.ne n with
+  | n + 1, _ =>
+    constructor
+    · intro h
+      constructor
+      · intro a b h
+        have := mkVector_inj (n := n+1) (a := a) (b := b)
+        simp only [Nat.add_one_ne_zero, false_or] at this
+        rw [← this]
+        apply eq_of_beq
+        rw [mkVector_beq_mkVector]
+        simpa
+      · intro a
+        suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
+          rw [mkVector_beq_mkVector] at this
+          simpa
+        simp
+    · intro h
+      constructor
+      · rintro ⟨a, ha⟩ ⟨b, hb⟩ h
+        simp at h
+        obtain ⟨hs, hi⟩ := Array.rel_of_isEqv h
+        ext i h
+        · simpa using hi _ (by omega)
+      · rintro ⟨a, ha⟩
+        simpa using Array.isEqv_self_beq ..
+
 /-! 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) :
@@ -920,20 +1028,6 @@ theorem map_empty (f : α → β) : map f #v[] = #v[] := by
   rw [map, mk.injEq]
   exact Array.map_empty f
 
-
-/--
-`Vector.ext` is an extensionality theorem.
-Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
--/
-@[ext]
-protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
-  apply Vector.toArray_inj
-  apply Array.ext
-  · rw [a.size_toArray, b.size_toArray]
-  · intro i hi _
-    rw [a.size_toArray] at hi
-    exact h i hi
-
 @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
   rcases v with ⟨data, rfl⟩
   simp