From d4805efb4b2d193467e61d38fc2601c28fd8d488 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 10 Aug 2022 08:06:41 +0000
Subject: [PATCH] feat(logic/equiv/list): add `countable` instances (#15960)

---
 src/data/finset/basic.lean |  5 +++--
 src/logic/equiv/list.lean  | 18 ++++++++++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
index 760853f00f45b..c45861de58ec9 100644
--- a/src/data/finset/basic.lean
+++ b/src/data/finset/basic.lean
@@ -146,8 +146,9 @@ namespace finset
 theorem eq_of_veq : ∀ {s t : finset α}, s.1 = t.1 → s = t
 | ⟨s, _⟩ ⟨t, _⟩ rfl := rfl
 
-@[simp] theorem val_inj {s t : finset α} : s.1 = t.1 ↔ s = t :=
-⟨eq_of_veq, congr_arg _⟩
+theorem val_injective : injective (val : finset α → multiset α) := λ _ _, eq_of_veq
+
+@[simp] theorem val_inj {s t : finset α} : s.1 = t.1 ↔ s = t := val_injective.eq_iff
 
 @[simp] theorem dedup_eq_self [decidable_eq α] (s : finset α) : dedup s.1 = s.1 :=
 s.2.dedup
diff --git a/src/logic/equiv/list.lean b/src/logic/equiv/list.lean
index ccfe8e61d4b7f..6c73ce175a80e 100644
--- a/src/logic/equiv/list.lean
+++ b/src/logic/equiv/list.lean
@@ -41,6 +41,9 @@ instance _root_.list.encodable : encodable (list α) :=
 ⟨encode_list, decode_list, λ l,
   by induction l with a l IH; simp [encode_list, decode_list, unpair_mkpair, encodek, *]⟩
 
+instance _root_.list.countable {α : Type*} [countable α] : countable (list α) :=
+by { haveI := encodable.of_countable α, apply_instance }
+
 @[simp] theorem encode_list_nil : encode (@nil α) = 0 := rfl
 @[simp] theorem encode_list_cons (a : α) (l : list α) :
   encode (a :: l) = succ (mkpair (encode a) (encode l)) := rfl
@@ -88,6 +91,10 @@ instance _root_.multiset.encodable : encodable (multiset α) :=
 ⟨encode_multiset, decode_multiset,
  λ s, by simp [encode_multiset, decode_multiset, encodek]⟩
 
+/-- If `α` is countable, then so is `multiset α`. -/
+instance _root_.multiset.countable {α : Type*} [countable α] : countable (multiset α) :=
+quotient.countable
+
 end finset
 
 /-- A listable type with decidable equality is encodable. -/
@@ -112,6 +119,9 @@ by { classical, exact (fintype.trunc_encodable α).out }
 /-- If `α` is encodable, then so is `vector α n`. -/
 instance _root_.vector.encodable [encodable α] {n} : encodable (vector α n) := subtype.encodable
 
+/-- If `α` is countable, then so is `vector α n`. -/
+instance _root_.vector.countable [countable α] {n} : countable (vector α n) := subtype.countable
+
 /-- If `α` is encodable, then so is `fin n → α`. -/
 instance fin_arrow [encodable α] {n} : encodable (fin n → α) :=
 of_equiv _ (equiv.vector_equiv_fin _ _).symm
@@ -123,12 +133,20 @@ of_equiv _ (equiv.pi_equiv_subtype_sigma (fin 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
  of_equiv {s : multiset α // s.nodup}
   ⟨λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, ⟨a, b⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
 
+/-- If `α` is countable, then so is `finset α`. -/
+instance _root_.finset.countable [countable α] : countable (finset α) :=
+finset.val_injective.countable
+
 -- TODO: Unify with `fintype_pi` and find a better name
 /-- When `α` is finite and `β` is encodable, `α → β` is encodable too. Because the encoding is not
 unique, we wrap it in `trunc` to preserve computability. -/