subtype vs set

Stream: general

[Kyle Miller]

In the spirit of having a canonical way of doing things, would it be possible for lean/mathlib to consistently use the has_coe_to_sort coercion of a set rather than ever using subtypes directly? Is there any reason not to do this? Dot notation still works fine.

It seems that in general it's nicer to work with sets than predicates, and most subtypes I've worked with aren't from raw predicates anyway. Eliminating // vs | (at the expense of introducing the coercion arrow) might make learning Lean just a little bit easier.

[Eric Wieser]

I'd argue that it's less irritating to use a lemma about subtypes with p = (∈ s) than it is to use one about sets with s = {x | p x}, especially if you then have decidable_pred (∈ {x | p x}) obligations that then appear

[Kyle Miller]

Hmm, should we have decidable_set s?

@[reducible]
def decidable_set {α : Type u} (s : set α) := decidable_pred (∈ s)

[Kyle Miller]

It might be more irritating to work with {x | p x} subtypes for lemmas, but it seems like it would be less irritating overall to not have these parallel worlds.

[Eric Wieser]

Removing the set world entirely would probably be awfully unpopular I suppose, even though α → Prop has analogous lattice structures.

[Yaël Dillies]

Well there's the issue of dot notation.

[Yaël Dillies]

although I already suggested we could make Lean look under thefunction namespace when dot notating on α → β.

[Yaël Dillies]

If we can do that, then we can also make it look under the set namespace when dot notating on α → Prop.

[Kyle Miller]

Beyond being unpopular, an issue with removing set is that there's no good way to normalize notation: is it p x or x ∈ p? It would be very nonstandard having to evaluate a predicate using ∈.

[Kyle Miller]

In case anyone's interested in a decidable_set, here's #9733 to start the discussion. I didn't go through and change all occurrences yet (and not all occurrences can be changed, since I put decidable_set in data.set.basic and not everything imports that).

[Eric Wieser]

I think decidable_mem would be a better name

[Kyle Miller]

It'd make sense also if it were for has_mem

[Kyle Miller]

(Though I sort of wish sometimes that has_mem were only for set, and that to use it for other types you define a coercion to set. This isn't so nice for finset though.)

[Kyle Miller]

Ok, #9733 is now about decidable_mem.