chore(data/fintype/vector, logic/equiv/list): split (#18226)

`array` and `d_array` do not exist in Lean 4; it's easier for porting if we put the stuff about those types in separate files.

src/computability/primrec.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import logic.equiv.array
 import logic.equiv.list
 import logic.function.iterate
 

src/data/array/lemmas.lean

@@ -270,32 +270,3 @@ read_foreach
 end map₂
 
 end array
-
-namespace equiv
-
-/-- The natural equivalence between length-`n` heterogeneous arrays
-and dependent functions from `fin n`. -/
-def d_array_equiv_fin {n : ℕ} (α : fin n → Type*) : d_array n α ≃ (Π i, α i) :=
-⟨d_array.read, d_array.mk, λ ⟨f⟩, rfl, λ f, rfl⟩
-
-/-- The natural equivalence between length-`n` arrays and functions from `fin n`. -/
-def array_equiv_fin (n : ℕ) (α : Type*) : array n α ≃ (fin n → α) :=
-d_array_equiv_fin _
-
-/-- The natural equivalence between length-`n` vectors and length-`n` arrays. -/
-def vector_equiv_array (α : Type*) (n : ℕ) : vector α n ≃ array n α :=
-(vector_equiv_fin _ _).trans (array_equiv_fin _ _).symm
-
-end equiv
-
-namespace array
-open function
-variable {n : ℕ}
-
-instance : traversable (array n) :=
-@equiv.traversable (flip vector n) _ (λ α, equiv.vector_equiv_array α n) _
-
-instance : is_lawful_traversable (array n) :=
-@equiv.is_lawful_traversable (flip vector n) _ (λ α, equiv.vector_equiv_array α n) _ _
-
-end array

src/data/fintype/array.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.fintype.pi
+import logic.equiv.array
+
+/-!
+# `array n α` is a fintype when `α` is.
+-/
+
+variables {α : Type*}
+
+instance d_array.fintype {n : ℕ} {α : fin n → Type*}
+  [∀ n, fintype (α n)] : fintype (d_array n α) :=
+fintype.of_equiv _ (equiv.d_array_equiv_fin _).symm
+
+instance array.fintype {n : ℕ} {α : Type*} [fintype α] : fintype (array n α) :=
+d_array.fintype

src/data/fintype/vector.lean

@@ -4,22 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.fintype.pi
-import data.array.lemmas
 import data.sym.basic
 
 /-!
-# `vector α n` is a fintype when `α` is.
+# `vector α n` and `sym α n` are fintypes when `α` is.
 -/
 
 variables {α : Type*}
 
-instance d_array.fintype {n : ℕ} {α : fin n → Type*}
-  [∀ n, fintype (α n)] : fintype (d_array n α) :=
-fintype.of_equiv _ (equiv.d_array_equiv_fin _).symm
-
-instance array.fintype {n : ℕ} {α : Type*} [fintype α] : fintype (array n α) :=
-d_array.fintype
-
 instance vector.fintype [fintype α] {n : ℕ} : fintype (vector α n) :=
 fintype.of_equiv _ (equiv.vector_equiv_fin _ _).symm
 

src/logic/equiv/array.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.vector.basic
+import logic.equiv.list
+import control.traversable.equiv
+
+/-!
+# Equivalences involving `array`
+
+We keep this separate from the file containing `list`-like equivalences as those have no future
+in mathlib4.
+-/
+
+namespace equiv
+
+/-- The natural equivalence between length-`n` heterogeneous arrays
+and dependent functions from `fin n`. -/
+def d_array_equiv_fin {n : ℕ} (α : fin n → Type*) : d_array n α ≃ (Π i, α i) :=
+⟨d_array.read, d_array.mk, λ ⟨f⟩, rfl, λ f, rfl⟩
+
+/-- The natural equivalence between length-`n` arrays and functions from `fin n`. -/
+def array_equiv_fin (n : ℕ) (α : Type*) : array n α ≃ (fin n → α) :=
+d_array_equiv_fin _
+
+/-- The natural equivalence between length-`n` vectors and length-`n` arrays. -/
+def vector_equiv_array (α : Type*) (n : ℕ) : vector α n ≃ array n α :=
+(vector_equiv_fin _ _).trans (array_equiv_fin _ _).symm
+
+end equiv
+
+namespace array
+open function
+variable {n : ℕ}
+
+instance : traversable (array n) :=
+@equiv.traversable (flip vector n) _ (λ α, equiv.vector_equiv_array α n) _
+
+instance : is_lawful_traversable (array n) :=
+@equiv.is_lawful_traversable (flip vector n) _ (λ α, equiv.vector_equiv_array α n) _ _
+
+end array
+
+/-- If `α` is encodable, then so is `array n α`. -/
+instance _root_.array.encodable {α} [encodable α] {n} : encodable (array n α) :=
+encodable.of_equiv _ (equiv.array_equiv_fin _ _)
+
+/-- If `α` is countable, then so is `array n α`. -/
+instance _root_.array.countable {α} [countable α] {n} : countable (array n α) :=
+countable.of_equiv _ (equiv.vector_equiv_array _ _)

src/logic/equiv/list.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.array.lemmas
 import data.finset.sort
+import data.vector.basic
 import logic.denumerable
 
 /-!
@@ -130,14 +130,6 @@ of_equiv _ (equiv.vector_equiv_fin _ _).symm
 instance fin_pi (n) (π : fin n → Type*) [∀ i, encodable (π i)] : encodable (Π i, π i) :=
 of_equiv _ (equiv.pi_equiv_subtype_sigma (fin n) π)
 
-/-- If `α` is encodable, then so is `array n α`. -/
-instance _root_.array.encodable [encodable α] {n} : encodable (array n α) :=
-of_equiv _ (equiv.array_equiv_fin _ _)
-
-/-- If `α` is countable, then so is `array n α`. -/
-instance _root_.array.countable [countable α] {n} : countable (array n α) :=
-countable.of_equiv _ (equiv.vector_equiv_array _ _)
-
 /-- If `α` is encodable, then so is `finset α`. -/
 instance _root_.finset.encodable [encodable α] : encodable (finset α) :=
 by haveI := decidable_eq_of_encodable α; exact