CoeSort for Finset

Stream: mathlib4

[Kyle Miller]

(Oughtn't s -> \beta work here? I remember in the past we didn't have a Finset-to-type coercion, but I wasn't sure why. Probably shouldn't discuss this in this thread.)

[Yaël Dillies]

(my recollection is that it's defeq but not synteq)

[Edward van de Meent]

there indeed is a difference; one prettyprints as ↑↑s, while the other prettyprints as { x // x ∈ s }

[Edward van de Meent]

i'm guessing ideally we'd want the following to work:

import Mathlib

variable (α : Type*) (s : Finset α) (a : α)

example : (a ∈ s) = (a ∈ (s : Set α)) := by with_reducible rfl

[Notification Bot]

4 messages were moved here from #mathlib4 > Convention for ∀ vs. Π by Kyle Miller.

[Kyle Miller]

I think it ought to be possible to fix this so that (s : Type) and ((s : Set A) : Type) give the same expression.

(In general, it seems like it ought to be possible for all set-likes for this to be the case, where the type coercion chains the set coercion with its type coercion. We could tweak the pretty printer so that it uses a single up arrow.)

[Edward van de Meent]

Kyle Miller said:

so that (s : Type) and ((s : Set A) : Type) give the same expression

with what reducibility option?

[Edward van de Meent]

reducible, instance or default?

[Edward van de Meent]

testing:

import Mathlib

variable (α : Type*) (s : Finset α) (a : α)
example : (s : Type _) = ((s : Set α) : Type _) := by with_reducible rfl -- fails
example : (s : Type _) = ((s : Set α) : Type _) := by with_reducible_and_instances rfl -- fails
example : (s : Type _) = ((s : Set α) : Type _) := by rfl -- succeeds

[Kyle Miller]

I mean the same expression, not defeq up to some reducibility setting.

[Edward van de Meent]

:hmm:

[Edward van de Meent]

so basically this:

attribute [-instance] Finset.instCoeSortType
universe u
variable (α : Type u)

instance : CoeSort (Finset α) (Type u) :=
  ⟨(·.toSet)⟩

variable (s : Finset α)
#check (s : Type u) -- ↑↑s : Type u
#check ((s : Set α) : Type u) -- ↑↑s : Type u

[Kyle Miller]

Yes, or equivalently

instance : CoeSort (Finset α) (Type u) :=
  ⟨fun s => (s : Set α)⟩