From a0b63deb043a07adddff6ced64c73e151bad9f16 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 14 Apr 2025 11:17:02 +1000
Subject: [PATCH] feat: updates to List/Array.Perm API (#7953)

This PR generalizes some typeclass hypotheses in the `List.Perm` API
(away from `DecidableEq`), and reproduces `List.Perm.mem_iff` for
`Array`, and fixes a mistake in the statement of `Array.Perm.extract`.
---
 src/Init/Data/Array/Perm.lean |  8 +++++++-
 src/Init/Data/List/Perm.lean  | 14 ++++++++++----
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/Init/Data/Array/Perm.lean b/src/Init/Data/Array/Perm.lean
index b42bad99dd..3e1570cc26 100644
--- a/src/Init/Data/Array/Perm.lean
+++ b/src/Init/Data/Array/Perm.lean
@@ -53,6 +53,12 @@ instance : Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α)) where
 
 theorem perm_comm {xs ys : Array α} : xs ~ ys ↔ ys ~ xs := ⟨Perm.symm, Perm.symm⟩
 
+theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a ∈ ys := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp at p
+  simpa using p.mem_iff
+
 theorem Perm.push (x y : α) {xs ys : Array α} (p : xs ~ ys) :
     (xs.push x).push y ~ (ys.push y).push x := by
   cases xs; cases ys
@@ -70,7 +76,7 @@ namespace Perm
 set_option linter.indexVariables false in
 theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
     (wlo : ∀ i, i < lo → xs[i]? = ys[i]?) (whi : ∀ i, hi ≤ i → xs[i]? = ys[i]?) :
-    (xs.extract lo (hi + 1)) ~ (ys.extract lo (hi + 1)) := by
+    (xs.extract lo hi) ~ (ys.extract lo hi) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp_all only [perm_toArray, List.getElem?_toArray, List.extract_toArray,
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index 1170e16348..c806cf3487 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 prelude
 import Init.Data.List.Pairwise
 import Init.Data.List.Erase
+import Init.Data.List.Find
 
 /-!
 # List Permutations
@@ -178,7 +179,7 @@ theorem Perm.singleton_eq (h : [a] ~ l) : [a] = l := singleton_perm.mp h
 
 theorem singleton_perm_singleton {a b : α} : [a] ~ [b] ↔ a = b := by simp
 
-theorem perm_cons_erase [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: l.erase a :=
+theorem perm_cons_erase [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: l.erase a :=
   let ⟨_, _, _, e₁, e₂⟩ := exists_erase_eq h
   e₂ ▸ e₁ ▸ perm_middle
 
@@ -268,7 +269,7 @@ theorem countP_eq_countP_filter_add (l : List α) (p q : α → Bool) :
     l.countP p = (l.filter q).countP p + (l.filter fun a => !q a).countP p :=
   countP_append .. ▸ Perm.countP_eq _ (filter_append_perm _ _).symm
 
-theorem Perm.count_eq [DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
+theorem Perm.count_eq [BEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
     count a l₁ = count a l₂ := p.countP_eq _
 
 /-
@@ -369,9 +370,9 @@ theorem perm_append_right_iff {l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ l
   refine ⟨fun p => ?_, .append_right _⟩
   exact (perm_append_left_iff _).1 <| perm_append_comm.trans <| p.trans perm_append_comm
 
-section DecidableEq
+section LawfulBEq
 
-variable [DecidableEq α]
+variable [BEq α] [LawfulBEq α]
 
 theorem Perm.erase (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase a ~ l₂.erase a :=
   if h₁ : a ∈ l₁ then
@@ -387,6 +388,11 @@ theorem cons_perm_iff_perm_erase {a : α} {l₁ l₂ : List α} :
   have : a ∈ l₂ := h.subset mem_cons_self
   exact ⟨this, (h.trans <| perm_cons_erase this).cons_inv⟩
 
+end LawfulBEq
+section DecidableEq
+
+variable [DecidableEq α]
+
 theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂ := by
   refine ⟨Perm.count_eq, fun H => ?_⟩
   induction l₁ generalizing l₂ with