feat: refactor DecidableEq (Array α)

src/Init/Data/Array/DecidableEq.lean

@@ -5,14 +5,15 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
+import Init.Data.BEq
 import Init.ByCases
 
 namespace Array
 
-theorem eq_of_isEqvAux
-    [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
-    (heqv : Array.isEqvAux a b hsz (fun x y => x = y) i hi)
-    (j : Nat) (hj : j < i) : a[j]'(Nat.lt_of_lt_of_le hj hi) = b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)) := by
+theorem rel_of_isEqvAux
+    (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
   induction i with
   | zero => contradiction
   | succ i ih =>
@@ -25,23 +26,28 @@ theorem eq_of_isEqvAux
       subst hj'
       exact heqv.left
 
-theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
-  simp [Array.isEqv]
-  split
-  next hsz =>
-   intro h
-   have aux := eq_of_isEqvAux a b hsz a.size (Nat.le_refl ..) h
-   exact ext a b hsz fun i h _ => aux i h
-  next => intro; contradiction
+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'⟩
+  · intro; contradiction
 
-theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) (h : i ≤ a.size) :
-    Array.isEqvAux a a rfl (fun x y => x = y) i h = true := by
+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
+  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) :
+    Array.isEqvAux a a rfl r i h = true := by
   induction i with
   | zero => simp [Array.isEqvAux]
   | succ i ih =>
-    simp_all only [isEqvAux, decide_True, Bool.and_self]
+    simp_all only [isEqvAux, Bool.and_self]
 
-theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
+theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Array α) : Array.isEqv a a (· == ·) = true := by
+  simp [isEqv, isEqvAux_self]
+
+theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (· = ·) = true := by
   simp [isEqv, isEqvAux_self]
 
 instance [DecidableEq α] : DecidableEq (Array α) :=