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 is
Sort 0
, there's a special case that you can only eliminate toSort 0
. Otherwise, inSort 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