feat(data/fintype): add choose_unique and construct inverses to bijec…

…tions (#421)

data/finset.lean

@@ -1593,6 +1593,23 @@ def attach_fin (s : finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : finset (fin
 @[simp] lemma card_attach_fin {n : ℕ} (s : finset ℕ) (h : ∀ m ∈ s, m < n) :
   (s.attach_fin h).card = s.card := multiset.card_pmap _ _ _
 
+section choose
+variables (p : α → Prop) [decidable_pred p] (l : finset α)
+
+def choose_x (hp : (∃! a, a ∈ l ∧ p a)) : { a // a ∈ l ∧ p a } :=
+multiset.choose_x p l.val hp
+
+def choose (hp : ∃! a, a ∈ l ∧ p a) : α := choose_x p l hp
+
+lemma choose_spec (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
+(choose_x p l hp).property
+
+lemma choose_mem (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l := (choose_spec _ _ _).1
+
+lemma choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) := (choose_spec _ _ _).2
+
+end choose
+
 theorem lt_wf {α} [decidable_eq α] : well_founded (@has_lt.lt (finset α) _) :=
 have H : subrelation (@has_lt.lt (finset α) _)
     (inv_image (<) card),

data/fintype.lean

@@ -5,7 +5,7 @@ Author: Mario Carneiro
 
 Finite types.
 -/
-import data.finset algebra.big_operators data.array.lemmas data.vector2
+import data.finset algebra.big_operators data.array.lemmas data.vector2 data.equiv.encodable
 universes u v
 
 variables {α : Type*} {β : Type*} {γ : Type*}
@@ -596,3 +596,53 @@ lemma fintype.card_equiv [fintype α] [fintype β] (e : α ≃ β) :
 fintype.card_congr (equiv_congr (equiv.refl α) e) ▸ fintype.card_perm
 
 end equiv
+
+namespace fintype
+
+section choose
+open fintype
+open equiv
+
+variables [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p]
+
+def choose_x (hp : ∃! a : α, p a) : {a // p a} :=
+⟨finset.choose p univ (by simp; exact hp), finset.choose_property _ _ _⟩
+
+def choose (hp : ∃! a, p a) : α := choose_x p hp
+
+lemma choose_spec (hp : ∃! a, p a) : p (choose p hp) :=
+(choose_x p hp).property
+
+end choose
+
+section bijection_inverse
+open function
+
+variables [fintype α] [decidable_eq α]
+variables [fintype β] [decidable_eq β]
+variables {f : α → β} 
+
+/-- `
+`bij_inv f` is the unique inverse to a bijection `f`. This acts
+  as a computable alternative to `function.inv_fun`. -/
+def bij_inv (f_bij : bijective f) (b : β) : α :=
+fintype.choose (λ a, f a = b)
+begin
+  rcases f_bij.right b with ⟨a', fa_eq_b⟩,
+  rw ← fa_eq_b,
+  exact ⟨a', ⟨rfl, (λ a h, f_bij.left h)⟩⟩
+end
+
+lemma left_inverse_bij_inv (f_bij : bijective f) : left_inverse (bij_inv f_bij) f :=
+λ a, f_bij.left (choose_spec (λ a', f a' = f a) _)
+
+lemma right_inverse_bij_inv (f_bij : bijective f) : right_inverse (bij_inv f_bij) f :=
+λ b, choose_spec (λ a', f a' = b) _
+
+lemma bijective_bij_inv (f_bij : bijective f) : bijective (bij_inv f_bij) :=
+⟨injective_of_left_inverse (right_inverse_bij_inv _),
+    surjective_of_has_right_inverse ⟨f, left_inverse_bij_inv _⟩⟩ 
+
+end bijection_inverse
+
+end fintype

data/list/basic.lean

@@ -4144,6 +4144,30 @@ h _ (list.nth_le_mem _ _ _) _ (list.nth_le_mem _ _ _)
 
 end tfae
 
+section choose
+variables (p : α → Prop) [decidable_pred p] (l : list α)
+
+def choose_x : Π l : list α, Π hp : (∃ a, a ∈ l ∧ p a), { a // a ∈ l ∧ p a }
+| [] hp := false.elim (exists.elim hp (assume a h, not_mem_nil a h.left))
+| (l :: ls) hp := if pl : p l then ⟨l, ⟨or.inl rfl, pl⟩⟩ else
+subtype.rec_on (choose_x ls
+  begin
+    rcases hp with ⟨a, rfl | a_mem_ls, pa⟩,
+    { exfalso; apply pl pa },
+    { exact ⟨a, a_mem_ls, pa⟩ }
+  end) (λ a ⟨a_mem_ls, pa⟩, ⟨a, ⟨or.inr a_mem_ls, pa⟩⟩)
+
+def choose (hp : ∃ a, a ∈ l ∧ p a) : α := choose_x p l hp
+
+lemma choose_spec (hp : ∃ a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
+(choose_x p l hp).property
+
+lemma choose_mem (hp : ∃ a, a ∈ l ∧ p a) : choose p l hp ∈ l := (choose_spec _ _ _).1
+
+lemma choose_property (hp : ∃ a, a ∈ l ∧ p a) : p (choose p l hp) := (choose_spec _ _ _).2
+
+end choose
+
 end list
 
 theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup

data/multiset.lean

@@ -2884,4 +2884,31 @@ lemma naturality {G H : Type* → Type*}
 quotient.induction_on x
 (by intro; simp [traverse,is_lawful_traversable.naturality] with functor_norm)
 
+section choose
+variables (p : α → Prop) [decidable_pred p] (l : multiset α)
+
+def choose_x : Π hp : (∃! a, a ∈ l ∧ p a), { a // a ∈ l ∧ p a } :=
+quotient.rec_on l (λ l' ex_unique, list.choose_x p l' (exists_of_exists_unique ex_unique)) begin
+  intros,
+  funext hp,
+  suffices all_equal : ∀ x y : { t // t ∈ b ∧ p t }, x = y,
+  { apply all_equal },
+  { rintros ⟨x, px⟩ ⟨y, py⟩,
+    rcases hp with ⟨z, ⟨z_mem_l, pz⟩, z_unique⟩,
+    congr,
+    calc x = z : z_unique x px
+    ...    = y : (z_unique y py).symm }
+end
+
+def choose (hp : ∃! a, a ∈ l ∧ p a) : α := choose_x p l hp
+
+lemma choose_spec (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
+(choose_x p l hp).property
+
+lemma choose_mem (hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l := (choose_spec _ _ _).1
+
+lemma choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) := (choose_spec _ _ _).2
+
+end choose
+
 end multiset