Zulip Chat Archive

Stream: Is there code for X?

Topic: Quotient of a fintype is a fintype


view this post on Zulip Eric Wieser (Dec 06 2020 at 10:55):

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 α β))"

view this post on Zulip Eric Wieser (Dec 06 2020 at 10:57):

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

view this post on Zulip Reid Barton (Dec 06 2020 at 10:57):

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

view this post on Zulip Eric Wieser (Dec 06 2020 at 10:57):

Or noncomputable theory, I suppose...

view this post on Zulip Eric Wieser (Dec 06 2020 at 11:09):

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

view this post on Zulip Eric Wieser (Dec 06 2020 at 11:11):

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

view this post on Zulip Reid Barton (Dec 06 2020 at 11:14):

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

view this post on Zulip Eric Wieser (Dec 06 2020 at 11:15):

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


Last updated: May 19 2021 at 00:40 UTC