chore(logic/encodable/basic): Rename encodable instances (#13396)

The instances were called `encodable.foo` instead of `foo.encodable` as the naming convention preconizes.

src/algebra/algebraic_card.lean

@@ -42,7 +42,7 @@ begin
     λ x, ulift.up (classical.some x.1.2),
   apply cardinal.mk_le_mk_mul_of_mk_preimage_le g (λ f, _),
   suffices : fintype (g ⁻¹' {f}),
-  { exact @mk_le_omega _ (@fintype.encodable _ this) },
+  { exact @mk_le_omega _ (@fintype.to_encodable _ this) },
   by_cases hf : f.1 = 0,
   { convert set.fintype_empty,
     apply set.eq_empty_iff_forall_not_mem.2 (λ x hx, _),

src/analysis/box_integral/partition/measure.lean

@@ -48,7 +48,7 @@ variables [fintype ι] (I : box ι)
 lemma measurable_set_coe : measurable_set (I : set (ι → ℝ)) :=
 begin
   rw [coe_eq_pi],
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   exact measurable_set.univ_pi (λ i, measurable_set_Ioc)
 end
 

src/computability/encoding.lean

@@ -207,7 +207,7 @@ end
 lemma fin_encoding.card_le_omega {α : Type u} (e : fin_encoding α) :
   (# α) ≤ ω :=
 begin
-  haveI : encodable e.Γ := fintype.encodable _,
+  haveI : encodable e.Γ := fintype.to_encodable _,
   exact e.to_encoding.card_le_omega,
 end
 

src/data/W/basic.lean

@@ -116,8 +116,6 @@ lemma depth_lt_depth_mk (a : α) (f : β a → W_type β) (i : β a) :
   depth (f i) < depth ⟨a, f⟩ :=
 nat.lt_succ_of_le (finset.le_sup (finset.mem_univ i))
 
-end W_type
-
 /-
 Show that W types are encodable when `α` is an encodable fintype and for every `a : α`, `β a` is
 encodable.
@@ -127,13 +125,11 @@ induction on `n` that these are all encodable. These auxiliary constructions are
 and of themselves, so we mark them as `private`.
 -/
 
-namespace encodable
-
 @[reducible] private def W_type' {α : Type*} (β : α → Type*)
     [Π a : α, fintype (β a)] [Π a : α, encodable (β a)] (n : ℕ) :=
 { t : W_type β // t.depth ≤ n}
 
-variables {α : Type*} {β : α → Type*} [Π a : α, fintype (β a)] [Π a : α, encodable (β a)]
+variables [Π a : α, encodable (β a)]
 
 private def encodable_zero : encodable (W_type' β 0) :=
 let f    : W_type' β 0 → empty := λ ⟨x, h⟩, false.elim $ not_lt_of_ge h (W_type.depth_pos _),
@@ -176,4 +172,4 @@ begin
   exact encodable.of_left_inverse f finv this
 end
 
-end encodable
+end W_type

src/data/rat/denumerable.lean

@@ -28,7 +28,7 @@ instance : denumerable ℚ :=
 begin
   let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.nat_abs.coprime x.2 },
   letI : infinite T := infinite.of_injective _ denumerable_aux.injective,
-  letI : encodable T := encodable.subtype,
+  letI : encodable T := subtype.encodable,
   letI : denumerable T := of_encodable_of_infinite T,
   exact denumerable.of_equiv T denumerable_aux
 end

src/data/set/countable.lean

@@ -185,7 +185,7 @@ lemma countable.insert {s : set α} (a : α) (h : countable s) : countable (inse
 countable_insert.2 h
 
 lemma finite.countable {s : set α} : finite s → countable s
-| ⟨h⟩ := trunc.nonempty (by exactI trunc_encodable_of_fintype s)
+| ⟨h⟩ := trunc.nonempty (by exactI fintype.trunc_encodable s)
 
 lemma subsingleton.countable {s : set α} (hs : s.subsingleton) : countable s :=
 hs.finite.countable

src/data/tprod.lean

@@ -23,7 +23,7 @@ construction/theorem that is easier to define/prove on binary products than on f
 * Then we can use the equivalence `list.tprod.pi_equiv_tprod` below (or enhanced versions of it,
   like a `measurable_equiv` for product measures) to get the construction on `Π i : ι, α i`, at
   least when assuming `[fintype ι] [encodable ι]` (using `encodable.sorted_univ`).
-  Using `local attribute [instance] fintype.encodable` we can get rid of the argument
+  Using `local attribute [instance] fintype.to_encodable` we can get rid of the argument
   `[encodable ι]`.
 
 ## Main definitions

src/logic/encodable/basic.lean

@@ -84,16 +84,16 @@ of_left_inverse e e.symm e.left_inv
 @[simp] theorem decode_of_equiv {α β} [encodable α] (e : β ≃ α) (n : ℕ) :
   @decode _ (of_equiv _ e) n = (decode α n).map e.symm := rfl
 
-instance nat : encodable ℕ :=
+instance _root_.nat.encodable : encodable ℕ :=
 ⟨id, some, λ a, rfl⟩
 
 @[simp] theorem encode_nat (n : ℕ) : encode n = n := rfl
 @[simp] theorem decode_nat (n : ℕ) : decode ℕ n = some n := rfl
 
-@[priority 100] instance is_empty [is_empty α] : encodable α :=
+@[priority 100] instance _root_.is_empty.to_encodable [is_empty α] : encodable α :=
 ⟨is_empty_elim, λ n, none, is_empty_elim⟩
 
-instance unit : encodable punit :=
+instance _root_.punit.encodable : encodable punit :=
 ⟨λ_, 0, λ n, nat.cases_on n (some punit.star) (λ _, none), λ _, by simp⟩
 
 @[simp] theorem encode_star : encode punit.star = 0 := rfl
@@ -102,7 +102,7 @@ instance unit : encodable punit :=
 @[simp] theorem decode_unit_succ (n) : decode punit (succ n) = none := rfl
 
 /-- If `α` is encodable, then so is `option α`. -/
-instance option {α : Type*} [h : encodable α] : encodable (option α) :=
+instance _root_.option.encodable {α : Type*} [h : encodable α] : encodable (option α) :=
 ⟨λ o, option.cases_on o nat.zero (λ a, succ (encode a)),
  λ n, nat.cases_on n (some none) (λ m, (decode α m).map some),
  λ o, by cases o; dsimp; simp [encodek, nat.succ_ne_zero]⟩
@@ -193,7 +193,7 @@ match bodd_div2 n with
 end
 
 /-- If `α` and `β` are encodable, then so is their sum. -/
-instance sum : encodable (α ⊕ β) :=
+instance _root_.sum.encodable : encodable (α ⊕ β) :=
 ⟨encode_sum, decode_sum, λ s,
   by cases s; simp [encode_sum, decode_sum, encodek]; refl⟩
 
@@ -206,7 +206,7 @@ instance sum : encodable (α ⊕ β) :=
 
 end sum
 
-instance bool : encodable bool :=
+instance _root_.bool.encodable : encodable bool :=
 of_equiv (unit ⊕ unit) equiv.bool_equiv_punit_sum_punit
 
 @[simp] theorem encode_tt : encode tt = 1 := rfl
@@ -226,7 +226,7 @@ begin
   simp [decode_sum]; cases bodd n; simp [decode_sum]; rw e; refl
 end
 
-noncomputable instance «Prop» : encodable Prop :=
+noncomputable instance _root_.Prop.encodable : encodable Prop :=
 of_equiv bool equiv.Prop_equiv_bool
 
 section sigma
@@ -241,7 +241,7 @@ def decode_sigma (n : ℕ) : option (sigma γ) :=
 let (n₁, n₂) := unpair n in
 (decode α n₁).bind $ λ a, (decode (γ a) n₂).map $ sigma.mk a
 
-instance sigma : encodable (sigma γ) :=
+instance _root_.sigma.encodable : encodable (sigma γ) :=
 ⟨encode_sigma, decode_sigma, λ ⟨a, b⟩,
   by simp [encode_sigma, decode_sigma, unpair_mkpair, encodek]⟩
 
@@ -258,7 +258,7 @@ section prod
 variables [encodable α] [encodable β]
 
 /-- If `α` and `β` are encodable, then so is their product. -/
-instance prod : encodable (α × β) :=
+instance _root_.prod.encodable : encodable (α × β) :=
 of_equiv _ (equiv.sigma_equiv_prod α β).symm
 
 @[simp] theorem decode_prod_val (n : ℕ) : decode (α × β) n =
@@ -289,7 +289,7 @@ def decode_subtype (v : ℕ) : option {a : α // P a} :=
 if h : P a then some ⟨a, h⟩ else none
 
 /-- A decidable subtype of an encodable type is encodable. -/
-instance subtype : encodable {a : α // P a} :=
+instance _root_.subtype.encodable : encodable {a : α // P a} :=
 ⟨encode_subtype, decode_subtype,
  λ ⟨v, h⟩, by simp [encode_subtype, decode_subtype, encodek, h]⟩
 
@@ -298,21 +298,21 @@ by cases a; refl
 
 end subtype
 
-instance fin (n) : encodable (fin n) :=
+instance _root_.fin.encodable (n) : encodable (fin n) :=
 of_equiv _ (equiv.fin_equiv_subtype _)
 
-instance int : encodable ℤ :=
+instance _root_.int.encodable : encodable ℤ :=
 of_equiv _ equiv.int_equiv_nat
 
-instance pnat : encodable ℕ+ :=
+instance _root_.pnat.encodable : encodable ℕ+ :=
 of_equiv _ equiv.pnat_equiv_nat
 
 /-- The lift of an encodable type is encodable. -/
-instance ulift [encodable α] : encodable (ulift α) :=
+instance _root_.ulift.encodable [encodable α] : encodable (ulift α) :=
 of_equiv _ equiv.ulift
 
 /-- The lift of an encodable type is encodable. -/
-instance plift [encodable α] : encodable (plift α) :=
+instance _root_.plift.encodable [encodable α] : encodable (plift α) :=
 of_equiv _ equiv.plift
 
 /-- If `β` is encodable and there is an injection `f : α → β`, then `α` is encodable as well. -/

src/logic/equiv/list.lean

@@ -37,7 +37,7 @@ def decode_list : ℕ → option (list α)
 
 /-- If `α` is encodable, then so is `list α`. This uses the `mkpair` and `unpair` functions from
 `data.nat.pairing`. -/
-instance list : encodable (list α) :=
+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, *]⟩
 
@@ -84,7 +84,7 @@ def decode_multiset (n : ℕ) : option (multiset α) :=
 coe <$> decode (list α) n
 
 /-- If `α` is encodable, then so is `multiset α`. -/
-instance multiset : encodable (multiset α) :=
+instance _root_.multiset.encodable : encodable (multiset α) :=
 ⟨encode_multiset, decode_multiset,
  λ s, by simp [encode_multiset, decode_multiset, encodek]⟩
 
@@ -94,22 +94,23 @@ end finset
 def encodable_of_list [decidable_eq α] (l : list α) (H : ∀ x, x ∈ l) : encodable α :=
 ⟨λ a, index_of a l, l.nth, λ a, index_of_nth (H _)⟩
 
-def trunc_encodable_of_fintype (α : Type*) [decidable_eq α] [fintype α] : trunc (encodable α) :=
+/-- A finite type is encodable. Because the encoding is not unique, we wrap it in `trunc` to
+preserve computability. -/
+def _root_.fintype.trunc_encodable (α : Type*) [decidable_eq α] [fintype α] : trunc (encodable α) :=
 @@quot.rec_on_subsingleton _
   (λ s : multiset α, (∀ x:α, x ∈ s) → trunc (encodable α)) _
   finset.univ.1
   (λ l H, trunc.mk $ encodable_of_list l H)
   finset.mem_univ
 
 /-- A noncomputable way to arbitrarily choose an ordering on a finite type.
-  It is not made into a global instance, since it involves an arbitrary choice.
-  This can be locally made into an instance with `local attribute [instance] fintype.encodable`. -/
-noncomputable def _root_.fintype.encodable (α : Type*) [fintype α] : encodable α :=
-by { classical, exact (encodable.trunc_encodable_of_fintype α).out }
+It is not made into a global instance, since it involves an arbitrary choice.
+This can be locally made into an instance with `local attribute [instance] fintype.to_encodable`. -/
+noncomputable def _root_.fintype.to_encodable (α : Type*) [fintype α] : encodable α :=
+by { classical, exact (fintype.trunc_encodable α).out }
 
 /-- If `α` is encodable, then so is `vector α n`. -/
-instance vector [encodable α] {n} : encodable (vector α n) :=
-encodable.subtype
+instance _root_.vector.encodable [encodable α] {n} : encodable (vector α n) := subtype.encodable
 
 /-- If `α` is encodable, then so is `fin n → α`. -/
 instance fin_arrow [encodable α] {n} : encodable (fin n → α) :=
@@ -119,26 +120,31 @@ instance fin_pi (n) (π : fin n → Type*) [∀ i, encodable (π i)] : encodable
 of_equiv _ (equiv.pi_equiv_subtype_sigma (fin n) π)
 
 /-- If `α` is encodable, then so is `array n α`. -/
-instance array [encodable α] {n} : encodable (array n α) :=
+instance _root_.array.encodable [encodable α] {n} : encodable (array n α) :=
 of_equiv _ (equiv.array_equiv_fin _ _)
 
 /-- If `α` is encodable, then so is `finset α`. -/
-instance finset [encodable α] : encodable (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⟩
 
+-- 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. -/
 def fintype_arrow (α : Type*) (β : Type*) [decidable_eq α] [fintype α] [encodable β] :
   trunc (encodable (α → β)) :=
 (fintype.trunc_equiv_fin α).map $
   λ f, encodable.of_equiv (fin (fintype.card α) → β) $
   equiv.arrow_congr f (equiv.refl _)
 
+/-- When `α` is finite and all `π a` are encodable, `Π a, π a` is encodable too. Because the
+encoding is not unique, we wrap it in `trunc` to preserve computability. -/
 def fintype_pi (α : Type*) (π : α → Type*) [decidable_eq α] [fintype α] [∀ a, encodable (π a)] :
   trunc (encodable (Π a, π a)) :=
-(encodable.trunc_encodable_of_fintype α).bind $ λ a,
-  (@fintype_arrow α (Σa, π a) _ _ (@encodable.sigma _ _ a _)).bind $ λ f,
-  trunc.mk $ @encodable.of_equiv _ _ (@encodable.subtype _ _ f _) (equiv.pi_equiv_subtype_sigma α π)
+(fintype.trunc_encodable α).bind $ λ a,
+  (@fintype_arrow α (Σa, π a) _ _ (@sigma.encodable _ _ a _)).bind $ λ f,
+  trunc.mk $ @encodable.of_equiv _ _ (@subtype.encodable _ _ f _) (equiv.pi_equiv_subtype_sigma α π)
 
 /-- The elements of a `fintype` as a sorted list. -/
 def sorted_univ (α) [fintype α] [encodable α] : list α :=
@@ -248,7 +254,7 @@ lemma raise_sorted : ∀ l n, list.sorted (≤) (raise l n)
 | (m :: l) n := (list.chain_iff_pairwise (@le_trans _ _)).1 (raise_chain _ _)
 
 /-- If `α` is denumerable, then so is `multiset α`. Warning: this is *not* the same encoding as used
-in `encodable.multiset`. -/
+in `multiset.encodable`. -/
 instance multiset : denumerable (multiset α) := mk' ⟨
   λ s : multiset α, encode $ lower ((s.map encode).sort (≤)) 0,
   λ n, multiset.map (of_nat α) (raise (of_nat (list ℕ) n) 0),
@@ -301,7 +307,7 @@ def raise'_finset (l : list ℕ) (n : ℕ) : finset ℕ :=
 ⟨raise' l n, (raise'_sorted _ _).imp (@ne_of_lt _ _)⟩
 
 /-- If `α` is denumerable, then so is `finset α`. Warning: this is *not* the same encoding as used
-in `encodable.finset`. -/
+in `finset.encodable`. -/
 instance finset : denumerable (finset α) := mk' ⟨
   λ s : finset α, encode $ lower' ((s.map (eqv α).to_embedding).sort (≤)) 0,
   λ n, finset.map (eqv α).symm.to_embedding (raise'_finset (of_nat (list ℕ) n) 0),

src/measure_theory/constructions/borel_space.lean

@@ -363,7 +363,7 @@ instance pi.opens_measurable_space_fintype {ι : Type*} {π : ι → Type*} [fin
   [Π i, measurable_space (π i)] [∀ i, second_countable_topology (π i)]
   [∀ i, opens_measurable_space (π i)] :
   opens_measurable_space (Π i, π i) :=
-by { letI := fintype.encodable ι, apply_instance }
+by { letI := fintype.to_encodable ι, apply_instance }
 
 instance prod.opens_measurable_space [second_countable_topology α] [second_countable_topology β] :
   opens_measurable_space (α × β) :=

src/measure_theory/constructions/pi.lean

@@ -83,7 +83,7 @@ lemma is_countably_spanning.pi {C : Π i, set (set (α i))}
   is_countably_spanning (pi univ '' pi univ C) :=
 begin
   choose s h1s h2s using hC,
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget,
   refine ⟨λ n, pi univ (λ i, s i (e n i)), λ n, mem_image_of_mem _ (λ i _, h1s i _), _⟩,
   simp_rw [(surjective_decode_iget (ι → ℕ)).Union_comp (λ x, pi univ (λ i, s i (x i))),
@@ -96,7 +96,7 @@ lemma generate_from_pi_eq {C : Π i, set (set (α i))}
   (hC : ∀ i, is_countably_spanning (C i)) :
   @measurable_space.pi _ _ (λ i, generate_from (C i)) = generate_from (pi univ '' pi univ C) :=
 begin
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   apply le_antisymm,
   { refine supr_le _, intro i, rw [comap_generate_from],
     apply generate_from_le, rintro _ ⟨s, hs, rfl⟩, dsimp,
@@ -277,7 +277,7 @@ begin
   refine le_antisymm _ _,
   { rw [measure.pi, to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i))],
     apply outer_measure.pi_pi_le },
-  { haveI : encodable ι := fintype.encodable ι,
+  { haveI : encodable ι := fintype.to_encodable ι,
     rw [← pi'_pi μ s],
     simp_rw [← pi'_pi μ s, measure.pi,
       to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i)), ← to_outer_measure_apply],
@@ -298,7 +298,7 @@ def finite_spanning_sets_in.pi {C : Π i, set (set (α i))}
   (measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) :=
 begin
   haveI := λ i, (hμ i).sigma_finite,
-  haveI := fintype.encodable ι,
+  haveI := fintype.to_encodable ι,
   refine ⟨λ n, pi univ (λ i, (hμ i).set ((decode (ι → ℕ) n).iget i)), λ n, _, λ n, _, _⟩;
   -- TODO (kmill) If this let comes before the refine, while the noncomputability checker
   -- correctly sees this definition is computable, the Lean VM fails to see the binding is
@@ -357,7 +357,7 @@ eq.symm $ pi_eq $ λ s hs, pi'_pi μ s
 
 @[simp] lemma pi_pi (s : Π i, set (α i)) : measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
 begin
-  haveI : encodable ι := fintype.encodable ι,
+  haveI : encodable ι := fintype.to_encodable ι,
   rw [← pi'_eq_pi, pi'_pi]
 end
 

src/measure_theory/function/strongly_measurable.lean

@@ -1693,7 +1693,7 @@ begin
   { rw tendsto_pi_nhds,
     exact λ p, ht_sf p.fst p.snd, },
   refine measurable_of_tendsto_metric (λ n, _) h_tendsto,
-  haveI : encodable (t_sf n).range, from fintype.encodable ↥(t_sf n).range,
+  haveI : encodable (t_sf n).range, from fintype.to_encodable ↥(t_sf n).range,
   have h_meas : measurable (λ (p : (t_sf n).range × α), u ↑p.fst p.snd),
   { have : (λ (p : ↥((t_sf n).range) × α), u ↑(p.fst) p.snd)
         = (λ (p : α × ((t_sf n).range)), u ↑(p.snd) p.fst) ∘ prod.swap := rfl,
@@ -1725,7 +1725,7 @@ begin
   { rw tendsto_pi_nhds,
     exact λ p, ht_sf p.fst p.snd, },
   refine strongly_measurable_of_tendsto _ (λ n, _) h_tendsto,
-  haveI : encodable (t_sf n).range, from fintype.encodable ↥(t_sf n).range,
+  haveI : encodable (t_sf n).range, from fintype.to_encodable ↥(t_sf n).range,
   have h_str_meas : strongly_measurable (λ (p : (t_sf n).range × α), u ↑p.fst p.snd),
   { refine strongly_measurable_iff_measurable_separable.2 ⟨_, _⟩,
     { have : (λ (p : ↥((t_sf n).range) × α), u ↑(p.fst) p.snd)

src/measure_theory/measurable_space.lean

@@ -735,7 +735,7 @@ end
 
 section fintype
 
-local attribute [instance] fintype.encodable
+local attribute [instance] fintype.to_encodable
 
 lemma measurable_set.pi_fintype [fintype δ] {s : set δ} {t : Π i, set (π i)}
   (ht : ∀ i ∈ s, measurable_set (t i)) : measurable_set (pi s t) :=

src/measure_theory/measurable_space_def.lean

@@ -140,7 +140,7 @@ by { rw compl_Inter, exact measurable_set.Union (λ b, (h b).compl) }
 
 section fintype
 
-local attribute [instance] fintype.encodable
+local attribute [instance] fintype.to_encodable
 
 lemma measurable_set.Union_fintype [fintype β] {f : β → set α} (h : ∀ b, measurable_set (f b)) :
   measurable_set (⋃ b, f b) :=

src/measure_theory/measure/hausdorff.lean

@@ -542,7 +542,7 @@ lemma mk_metric_le_liminf_sum {β : Type*} {ι : β → Type*} [hι : ∀ n, fin
   (m : ℝ≥0∞ → ℝ≥0∞) :
   mk_metric m s ≤ liminf l (λ n, ∑ i, m (diam (t n i))) :=
 begin
-  haveI : ∀ n, encodable (ι n), from λ n, fintype.encodable _,
+  haveI : ∀ n, encodable (ι n), from λ n, fintype.to_encodable _,
   simpa only [tsum_fintype] using mk_metric_le_liminf_tsum s r hr t ht hst m,
 end