feat: LawfulBEq (Array α) ↔ LawfulBEq α

src/Init/Data/Array/DecidableEq.lean

@@ -13,9 +13,9 @@ import Init.ByCases
 namespace Array
 
 theorem rel_of_isEqvAux
-    (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
+    {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
     (heqv : Array.isEqvAux a b hsz r i hi)
-    (j : Nat) (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
+    {j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
   induction i with
   | zero => contradiction
   | succ i ih =>
@@ -28,7 +28,7 @@ theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
-theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
+theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
     (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
   induction i with
   | zero => simp [Array.isEqvAux]
@@ -36,18 +36,18 @@ theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size
     simp only [isEqvAux, Bool.and_eq_true]
     exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
 
-theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
+theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
     Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
   simp only [isEqv]
   split <;> rename_i h
-  · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
+  · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
 theorem isEqv_iff_rel (a b : Array α) (r) :
     Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
-  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
+  ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
     simp only [isEqv, ← h, ↓reduceDIte]
-    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
+    exact isEqvAux_of_rel h (by simp [h]) w⟩
 
 theorem isEqv_eq_decide (a b : Array α) (r) :
     Array.isEqv a b r =
@@ -67,7 +67,7 @@ theorem isEqv_eq_decide (a b : Array α) (r) :
   simp [isEqv_eq_decide, List.isEqv_eq_decide]
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
-  have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
+  have ⟨h, h'⟩ := rel_of_isEqv h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
 
 theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :

src/Init/Data/Array/Lemmas.lean

@@ -11,6 +11,7 @@ import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
 import Init.Data.Array.Mem
+import Init.Data.Array.DecidableEq
 import Init.TacticsExtra
 
 /-!
@@ -69,6 +70,9 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
     rfl
   · simp [getElem?_eq_none_iff.2 (by simpa using h)]
 
+theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+  simp
+
 end Array
 
 namespace List
@@ -713,6 +717,43 @@ 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