feat: lemmas about permutations (#7912)

This PR adds `List.Perm.take/drop`, and `Array.Perm.extract`,
restricting permutations to sublist / subarrays when they are constant
elsewhere.

src/Init/Data/Array/Perm.lean

@@ -65,4 +65,20 @@ theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < x
   simp only [swap, perm_iff_toList_perm, toList_set]
   apply set_set_perm
 
+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
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp_all only [perm_toArray, List.getElem?_toArray, List.extract_toArray,
+    List.extract_eq_drop_take]
+  apply List.Perm.take' (w := fun i h => by simpa using whi (lo + i) (by omega))
+  apply List.Perm.drop' (w := wlo)
+  exact h
+
+end Perm
+
 end Array

src/Init/Data/List/Nat/Perm.lean

@@ -54,4 +54,23 @@ theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j
       subst t
       apply set_set_perm' _ _ (by omega)
 
+namespace Perm
+
+/-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/
+theorem take' {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → l₁[j]? = l₂[j]?) :
+    (l₁.take i) ~ (l₂.take i) := by
+  apply h.take
+  ext1 j
+  simpa using w (i + j) (by omega)
+
+/-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/
+theorem drop' {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → l₁[j]? = l₂[j]?) :
+    (l₁.drop i) ~ (l₂.drop i) := by
+  apply h.drop
+  ext1
+  simp only [getElem?_take]
+  split <;> simp_all
+
+end Perm
+
 end List

src/Init/Data/List/Perm.lean

@@ -536,4 +536,16 @@ theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
       simp only [insertIdx, modifyTailIdx]
       refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)
 
+namespace Perm
+
+theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n = l₂.drop n) :
+    (l₁.take n) ~ (l₂.take n) := by
+  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, w, perm_append_right_iff] at h
+
+theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₂.take n = l₁.take n) :
+    (l₁.drop n) ~ (l₂.drop n) := by
+  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, w, perm_append_left_iff] at h
+
+end Perm
+
 end List