feat: add LawfulBEq instance for Vector (#1104)

Co-authored-by: François G. Dorais <[email protected]>

Batteries/Data/Vector/Basic.lean

@@ -39,8 +39,6 @@ namespace Vector
 @[deprecated "Use `#v[]`." (since := "2024-11-27")]
 def empty (α : Type u) : Vector α 0 := #v[]
 
-proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n)
-
 /--
 Returns `true` when all elements of the vector are pairwise distinct using `==` for comparison.
 -/

Batteries/Data/Vector/Lemmas.lean

@@ -203,6 +203,13 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
     (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
 
+theorem isEqv_eq_toArray_isEqv_toArray (a b : Vector α n) :
+    a.isEqv b r = a.toArray.isEqv b.toArray r :=
+  match a, b with | ⟨_,_⟩, ⟨_,_⟩ => mk_isEqv_mk ..
+
+theorem beq_eq_toArray_beq [BEq α] (a b : Vector α n) : (a == b) = (a.toArray == b.toArray) := by
+  simp [(· == ·), isEqv_eq_toArray_isEqv_toArray]
+
 /-! ### toList lemmas -/
 
 theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
@@ -291,3 +298,9 @@ instance instDecidableExistsVectorZero (P : Vector α 0 → Prop) [Decidable (P
 instance instDecidableExistsVectorSucc (P : Vector α (n+1) → Prop)
     [Decidable (∀ (x : α) (v : Vector α n), ¬ P (v.push x))] : Decidable (∃ v, P v) :=
   decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+
+instance (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α n) where
+  rfl {a} := by simp_all [beq_eq_toArray_beq]
+  eq_of_beq {a b h} := by
+    apply toArray_injective
+    simp_all [beq_eq_toArray_beq]