Quotient of a fintype is a fintype

Stream: Is there code for X?

[Eric Wieser]

This is complaining about a missing instance, but I'm pretty sure the instance is in mathlib somewhere:

import group_theory.perm.sign

def mod_sum_congr (α β : Type*) : setoid (equiv.perm (α ⊕ β)) :=
{ r := λ σ₁ σ₂, ∃ sl sr, σ₁ = σ₂ * equiv.sum_congr sl sr,
  iseqv := ⟨
    λ σ, ⟨1, 1, by simp [equiv.perm.mul_def, equiv.perm.one_def]⟩,
    λ σ₁ σ₂ ⟨sl, sr, h⟩, ⟨sl⁻¹, sr⁻¹, by {
      rw [h, mul_assoc],
      simp [equiv.perm.mul_def, equiv.perm.inv_def]}⟩,
    λ σ₁ σ₂ σ₃ ⟨sl₁₂, sr₁₂, h₁₂⟩ ⟨sl₂₃, sr₂₃, h₂₃⟩, ⟨sl₂₃ * sl₁₂, sr₂₃ * sr₁₂, by {
      rw [h₁₂, h₂₃, mul_assoc],
      simp [equiv.perm.mul_def, equiv.perm.inv_def]}⟩
⟩}

variables (α β : Type*) [fintype α] [fintype β] [decidable_eq α] [decidable_eq β]

#check (infer_instance : fintype (equiv.perm $ α ⊕ β))  -- ok

#check ∑ σ : quotient (mod_sum_congr α β), 1
-- failed to synthesize type class instance for "fintype (quotient (mod_sum_congr α β))"

[Eric Wieser]

Ah, it seems docs#quotient.fintype needs the setoid to be decidable

[Reid Barton]

This needs some decidability of the equivalence relation ... yes

[Eric Wieser]

Or noncomputable theory, I suppose...

[Eric Wieser]

Any tips for how to construct the decidable instance constructively? I know how I'd write an algorithm to decide the statement, but I don't really know how to transfer them to lean; in particular, I don;t know how to state pa and pb in a way that lean already knows is decidable.

instance {α β : Type*} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
  decidable_rel (mod_sum_congr α β).r :=
λ σ₁ σ₂, begin
  dunfold mod_sum_congr,
  dsimp,
  let pa := ∀ a₁, ∃ a₂, (σ₂⁻¹ * σ₁) (sum.inl a₁) = sum.inl a₂,
  let pb := ∀ b₁, ∃ b₂, (σ₂⁻¹ * σ₁) (sum.inr b₁) = sum.inr b₂,
  haveI : decidable pa := sorry,
  haveI : decidable pb := sorry,
  by_cases ha : pa; dsimp only [pa] at ha;
  by_cases hb : pb; dsimp only [pb] at hb,
  { apply decidable.is_true,
    sorry },
  { exfalso, sorry },
  { exfalso, sorry },
  { apply decidable.is_false,
    sorry }
end

[Eric Wieser]

pa should be trivially decidable via exhaustive iteration over the fintype α, right?

[Reid Barton]

are there already decidable_eq/fintype instances for equivs between two decidable_eq+fintype types?

[Eric Wieser]

Nevermind:

instance {α β : Type*} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
  decidable_rel (mod_sum_congr α β).r :=
λ σ₁ σ₂, begin
  dunfold mod_sum_congr,
  apply_instance,
end

I must have been rememvering an older version where I used sigma types instead of sum type