Zulip Chat Archive

Stream: general

Topic: should fintype take a sort?


Chris Hughes (Aug 06 2018 at 14:40):

This instance would be possible if fintype took a sort instead of a Type. Is it worth changing?
instance (p : fin 3 → Prop) [decidable_pred p] : fintype (Π a, p a → fin 3) := by apply_instance

Mario Carneiro (Aug 06 2018 at 14:44):

I thought about it, I have also seen this come up, but I don't know a clean way to do it without making lots of later stuff harder

Chris Hughes (Aug 06 2018 at 14:45):

What would be harder?

Mario Carneiro (Aug 06 2018 at 14:45):

you have to ulift somewhere, and this will affect proofs that don't care about Prop

Mario Carneiro (Aug 06 2018 at 14:48):

of course another way to solve the particular problem you show is to have a second pi instance for Props

Chris Hughes (Aug 06 2018 at 14:53):

I forgot that list didn't take a Sort.

Mario Carneiro (Aug 06 2018 at 14:56):

Actually, I'm not sure it can be done at all, assuming that list and finset stay as is

Mario Carneiro (Aug 06 2018 at 14:57):

What would be the type of fintype? If it is Sort u -> Type u then it bumps the universe level in unwanted circumstances (i.e. fintype nat : Type 1), and if it is Sort u -> Sort (max 1 u) then you can't define it

Mario Carneiro (Aug 06 2018 at 14:59):

since Sort (max 1 u) = Sort (?+1) is unsolvable (you would need a pred u function but that doesn't exist)

Chris Hughes (Aug 06 2018 at 17:02):

Is there any reason not to just make everything a Sort, just in case some random thing like this comes up where it's useful?

Simon Hudon (Aug 06 2018 at 18:08):

I think the main thing has to do with elimination. If your type isSort 0, there's a special case that you can only eliminate to Sort 0. Otherwise, in Sort 1, you can eliminate anywhere you like.

Simon Hudon (Aug 06 2018 at 18:16):

Btw, your instance type checks for me. Are you sure your issues have to do with universes?

Chris Hughes (Aug 06 2018 at 18:17):

It type checks, but it can't synthesize the instance

Chris Hughes (Aug 06 2018 at 18:19):

But if there was an instance saying Pi p : Prop, fintype p it would synthesize the instance from pi.fintype

Simon Hudon (Aug 06 2018 at 18:41):

I think you could make it work with an instance like this:

instance pi.fintype' {α : Prop} {β : α  Type*}
  [decidable α] [a, fintype (β a)] : fintype (Πa, β a) :=

Chris Hughes (Aug 06 2018 at 18:47):

I think the main thing has to do with elimination. If your type isSort 0, there's a special case that you can only eliminate to Sort 0. Otherwise, in Sort 1, you can eliminate anywhere you like.

So that makes sense for making inductive types Types rather than sorts, but for functions defined on an arbitrary Type, I don't see a downside.

Chris Hughes (Aug 06 2018 at 18:59):

I should probably PR both of these

instance decidable_eq_pfun_fintype (P : Prop) [decidable P] (α : P  Type*) [Π hp : P, fintype (α hp)]
  [Π hp : P, decidable_eq (α hp)] : decidable_eq (Π hp : P, α hp) :=
λ f g, if hp : P then decidable_of_iff (f hp = g hp) (⟨λ h, funext $ λ _, h, λ h, congr_fun h _⟩)
else is_true (funext $ λ h, (hp h).elim)

instance fintype_pfun (P : Prop) [decidable P] (α : P  Type*) [Π hp : P, fintype (α hp)]
  [Π hp : P, decidable_eq (α hp)] : fintype (Π hp : P, α hp) :=
if hp : P then fintype.of_equiv (α hp) ⟨λ a _, a, λ f, f hp, λ _, rfl, λ _, rfl
else finset.singleton (λ h, (hp h).elim), λ x, by simp [hp, funext_iff]

Simon Hudon (Aug 06 2018 at 19:11):

but for functions defined on an arbitrary Type, I don't see a downside.

I agree. Although, I find that universe constraints have a way of propagating to infect every definition once you have one. Being more polymorphic seems easier said than done.


Last updated: Dec 20 2023 at 11:08 UTC