feat(data/fintype): finite choices, computably

data/fintype.lean

@@ -268,3 +268,62 @@ set_fintype _
 
 instance set.fintype [fintype α] [decidable_eq α] : fintype (set α) :=
 pi.fintype
+
+def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
+  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
+  ∀ (l : list ι), (∀ i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
+| []     f := ⟦λ i, false.elim⟧
+| (i::l) f := begin
+  refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
+    (quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
+    _ _,
+  exact λ a l, ⟦λ j h,
+    if e : j = i then by rw e; exact a else
+    l _ (h.resolve_left e)⟧,
+  refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
+  by_cases e : j = i; simp [e],
+  { subst j, exact h₁ },
+  { exact h₂ _ _ }
+end
+
+theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
+  {α : ι → Type*} [S : ∀ i, setoid (α i)] :
+  ∀ (l : list ι) (f : ∀ i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
+| []     f := quotient.sound (λ i h, h.elim)
+| (i::l) f := begin
+  simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
+  refine quotient.sound (λ j h, _),
+  by_cases e : j = i; simp [e],
+  subst j, refl
+end
+
+def quotient.fin_choice {ι : Type*} [fintype ι] [decidable_eq ι]
+  {α : ι → Type*} [S : ∀ i, setoid (α i)]
+  (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
+quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
+    @quotient (Π i ∈ l, α i) (by apply_instance))
+    finset.univ.1
+    (λ l, quotient.fin_choice_aux l (λ i _, f i))
+    (λ a b h, begin
+      have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
+      simp [quotient.out_eq] at this,
+      simp [this],
+      let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
+      refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
+      congr' 1, exact quotient.sound h,
+    end))
+  (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
+  (λ a b h, quotient.sound $ λ i, h _ _)
+
+
+theorem quotient.fin_choice_eq {ι : Type*} [fintype ι] [decidable_eq ι]
+  {α : ι → Type*} [∀ i, setoid (α i)]
+  (f : ∀ i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
+begin
+  let q, swap, change quotient.lift_on q _ _ = _,
+  have : q = ⟦λ i h, f i⟧,
+  { dsimp [q],
+    exact quotient.induction_on
+      (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
+  simp [this], exact setoid.refl _
+end

data/quot.lean

@@ -41,6 +41,21 @@ noncomputable def quotient.out [s : setoid α] : quotient s → α := quot.out
 theorem quotient.mk_out [s : setoid α] (a : α) : ⟦a⟧.out ≈ a :=
 quotient.exact (quotient.out_eq _)
 
+instance pi_setoid {ι : Sort*} {α : ι → Sort*} [∀ i, setoid (α i)] : setoid (Π i, α i) :=
+{ r := λ a b, ∀ i, a i ≈ b i,
+  iseqv := ⟨
+    λ a i, setoid.refl _,
+    λ a b h i, setoid.symm (h _),
+    λ a b c h₁ h₂ i, setoid.trans (h₁ _) (h₂ _)⟩ }
+
+noncomputable def quotient.choice {ι : Type*} {α : ι → Type*} [S : ∀ i, setoid (α i)]
+  (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
+⟦λ i, (f i).out⟧
+
+theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [∀ i, setoid (α i)]
+  (f : ∀ i, α i) : quotient.choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
+quotient.sound $ λ i, quotient.mk_out _
+
 /-- `trunc α` is the quotient of `α` by the always-true relation. This
   is related to the propositional truncation in HoTT, and is similar
   in effect to `nonempty α`, but unlike `nonempty α`, `trunc α` is data,