feat(data/fintype): computable trunc bijection from fin (#10141)

When a type `X` lacks decidable equality, there is still computably a bijection `fin (card X) -> X` using `trunc`.

Also, move `fintype.equiv_fin_of_forall_mem_list` to `list.nodup.nth_le_equiv_of_forall_mem_list`.

src/data/equiv/list.lean

@@ -164,7 +164,7 @@ def fintype_equiv_fin {α} [fintype α] [encodable α] :
 begin
   haveI : decidable_eq α := encodable.decidable_eq_of_encodable _,
   transitivity,
-  { exact fintype.equiv_fin_of_forall_mem_list mem_sorted_univ (sorted_univ_nodup α) },
+  { exact ((sorted_univ_nodup α).nth_le_equiv_of_forall_mem_list _ mem_sorted_univ).symm },
   exact equiv.cast (congr_arg _ (length_sorted_univ α))
 end
 

src/data/fintype/basic.lean

@@ -8,6 +8,7 @@ import data.finset.option
 import data.finset.pi
 import data.finset.powerset
 import data.finset.prod
+import data.list.nodup_equiv_fin
 import data.sym.basic
 import data.ulift
 import group_theory.perm.basic
@@ -297,32 +298,26 @@ by have := and.intro univ.2 mem_univ_val;
 /-- `card α` is the number of elements in `α`, defined when `α` is a fintype. -/
 def card (α) [fintype α] : ℕ := (@univ α _).card
 
-/-- If `l` lists all the elements of `α` without duplicates, then `α ≃ fin (l.length)`. -/
-def equiv_fin_of_forall_mem_list {α} [decidable_eq α]
-  {l : list α} (h : ∀ x : α, x ∈ l) (nd : l.nodup) : α ≃ fin (l.length) :=
-⟨λ a, ⟨_, list.index_of_lt_length.2 (h a)⟩,
- λ i, l.nth_le i.1 i.2,
- λ a, by simp,
- λ ⟨i, h⟩, fin.eq_of_veq $ list.nodup_iff_nth_le_inj.1 nd _ _
-   (list.index_of_lt_length.2 (list.nth_le_mem _ _ _)) h $ by simp⟩
+/-- There is (computably) an equivalence between `α` and `fin (card α)`.
 
-/-- There is (computably) a bijection between `α` and `fin (card α)`.
-
-Since it is not unique, and depends on which permutation
-of the universe list is used, the bijection is wrapped in `trunc` to
+Since it is not unique and depends on which permutation
+of the universe list is used, the equivalence is wrapped in `trunc` to
 preserve computability.
 
 See `fintype.equiv_fin` for the noncomputable version,
 and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq`
 for an equiv `α ≃ fin n` given `fintype.card α = n`.
+
+See `fintype.trunc_fin_bijection` for a version without `[decidable_eq α]`.
 -/
 def trunc_equiv_fin (α) [decidable_eq α] [fintype α] : trunc (α ≃ fin (card α)) :=
-by unfold card finset.card; exact
-quot.rec_on_subsingleton (@univ α _).1
-  (λ l (h : ∀ x : α, x ∈ l) (nd : l.nodup), trunc.mk (equiv_fin_of_forall_mem_list h nd))
-  mem_univ_val univ.2
+by { unfold card finset.card,
+     exact quot.rec_on_subsingleton (@univ α _).1
+       (λ l (h : ∀ x : α, x ∈ l) (nd : l.nodup),
+         trunc.mk (nd.nth_le_equiv_of_forall_mem_list _ h).symm)
+       mem_univ_val univ.2 }
 
-/-- There is a (noncomputable) bijection between `α` and `fin (card α)`.
+/-- There is (noncomputably) an equivalence between `α` and `fin (card α)`.
 
 See `fintype.trunc_equiv_fin` for the computable version,
 and `fintype.trunc_equiv_fin_of_card_eq` and `fintype.equiv_fin_of_card_eq`
@@ -331,6 +326,23 @@ for an equiv `α ≃ fin n` given `fintype.card α = n`.
 noncomputable def equiv_fin (α) [fintype α] : α ≃ fin (card α) :=
 by { letI := classical.dec_eq α, exact (trunc_equiv_fin α).out }
 
+/-- There is (computably) a bijection between `fin (card α)` and `α`.
+
+Since it is not unique and depends on which permutation
+of the universe list is used, the bijection is wrapped in `trunc` to
+preserve computability.
+
+See `fintype.trunc_equiv_fin` for a version that gives an equivalence
+given `[decidable_eq α]`.
+-/
+def trunc_fin_bijection (α) [fintype α] :
+  trunc {f : fin (card α) → α // bijective f} :=
+by { dunfold card finset.card,
+     exact quot.rec_on_subsingleton (@univ α _).1
+       (λ l (h : ∀ x : α, x ∈ l) (nd : l.nodup),
+         trunc.mk (nd.nth_le_bijection_of_forall_mem_list _ h))
+       mem_univ_val univ.2 }
+
 instance (α : Type*) : subsingleton (fintype α) :=
 ⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext_iff, h₁, h₂]⟩
 

src/data/list/nodup_equiv_fin.lean

@@ -8,13 +8,18 @@ import data.list.sort
 import data.list.duplicate
 
 /-!
-# Isomorphism between `fin (length l)` and `{x // x ∈ l}`
+# Equivalence between `fin (length l)` and elements of a list
 
-Given a list `l,
+Given a list `l`,
 
-* if `l` has no duplicates, then `list.nodup.nth_le_equiv` is the bijection between `fin (length l)`
-  and `{x // x ∈ l}` sending `⟨i, hi⟩` to `⟨nth_le l i hi, _⟩` with the inverse sending `⟨x, hx⟩` to
-  `⟨index_of x l, _⟩`;
+* if `l` has no duplicates, then `list.nodup.nth_le_equiv` is the equivalence between
+  `fin (length l)` and `{x // x ∈ l}` sending `⟨i, hi⟩` to `⟨nth_le l i hi, _⟩` with the inverse
+  sending `⟨x, hx⟩` to `⟨index_of x l, _⟩`;
+
+* if `l` has no duplicates and contains every element of a type `α`, then
+  `list.nodup.nth_le_equiv_of_forall_mem_list` defines an equivalence between
+  `fin (length l)` and `α`;  if `α` does not have decidable equality, then
+  there is a bijection `list.nodup.nth_le_bijection_of_forall_mem_list`;
 
 * if `l` is sorted w.r.t. `(<)`, then `list.sorted.nth_le_iso` is the same bijection reinterpreted
   as an `order_iso`.
@@ -27,20 +32,38 @@ variable {α : Type*}
 
 namespace nodup
 
+/-- If `l` lists all the elements of `α` without duplicates, then `list.nth_le` defines
+a bijection `fin l.length → α`.  See `list.nodup.nth_le_equiv_of_forall_mem_list`
+for a version giving an equivalence when there is decidable equality. -/
+@[simps]
+def nth_le_bijection_of_forall_mem_list (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) :
+  {f : fin l.length → α // function.bijective f} :=
+⟨λ i, l.nth_le i i.property, λ i j h, fin.ext $ (nd.nth_le_inj_iff _ _).1 h,
+ λ x, let ⟨i, hi, hl⟩ := list.mem_iff_nth_le.1 (h x) in ⟨⟨i, hi⟩, hl⟩⟩
+
 variable [decidable_eq α]
 
-/-- If `l` has no duplicates, then `list.nth_le` defines a bijection between `fin (length l)` and
+/-- If `l` has no duplicates, then `list.nth_le` defines an equivalence between `fin (length l)` and
 the set of elements of `l`. -/
+@[simps]
 def nth_le_equiv (l : list α) (H : nodup l) : fin (length l) ≃ {x // x ∈ l} :=
 { to_fun := λ i, ⟨nth_le l i i.2, nth_le_mem l i i.2⟩,
   inv_fun := λ x, ⟨index_of ↑x l, index_of_lt_length.2 x.2⟩,
   left_inv := λ i, by simp [H],
   right_inv := λ x, by simp }
 
-variables {l : list α} (H : nodup l) (x : {x // x ∈ l}) (i : fin (length l))
-
-@[simp] lemma coe_nth_le_equiv_apply : (H.nth_le_equiv l i : α) = nth_le l i i.2 := rfl
-@[simp] lemma coe_nth_le_equiv_symm_apply : ((H.nth_le_equiv l).symm x : ℕ) = index_of ↑x l := rfl
+/-- If `l` lists all the elements of `α` without duplicates, then `list.nth_le` defines
+an equivalence between `fin l.length` and `α`.
+
+See `list.nodup.nth_le_bijection_of_forall_mem_list` for a version without
+decidable equality. -/
+@[simps]
+def nth_le_equiv_of_forall_mem_list (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) :
+  fin l.length ≃ α :=
+{ to_fun := λ i, l.nth_le i i.2,
+  inv_fun := λ a, ⟨_, index_of_lt_length.2 (h a)⟩,
+  left_inv := λ i, by simp [nd],
+  right_inv := λ a, by simp }
 
 end nodup