Generic `has_subset`?

Stream: general

[Yury G. Kudryashov]

What do you think about replacing all our has_subset instances with the following generic instance?

instance {α : Type*} {β : out_param (Type*)} [out_param (has_mem β α)] : has_subset α :=
⟨λ s t, ∀ {{x : β}}, x ∈ s → x ∈ t⟩

[Yury G. Kudryashov]

(and similarly for has_ssubset)

[Yaël Dillies]

Are you aware of #11381?

[Yaël Dillies]

It's a less hardcoding proposition to make more lemmas available cross-structure

[Yaël Dillies]

The only problem I see is that there are still a few lemmas that can't be generalized (although arguably not that much and not the important ones) and that I get elaboration issues as ⊆ acts like a function.

[Yaël Dillies]

@Anne Baanen might actually have things to say

[Yaël Dillies]

Sorry to ping you virtually everywhere :grinning:

[Yury G. Kudryashov]

I'm aware of #11381 but I think that our current has_subset/has_ssubset are too general: all instances I know about have this generic form.

[Yury G. Kudryashov]

So, we can actually replace subset/ssubset with defs in terms of has_mem.

[Yaël Dillies]

or just a general instance in terms of has_mem?

[Yaël Dillies]

Thinking again, that's probably not a good idea to trigger typeclass search when there's only one satisfying typeclass.

[Yury G. Kudryashov]

If we're going to have only one instance, then I prefer a def.

[Yaël Dillies]

One thing you have to consider is whether we'll ever need definitional properties for ⊂.

[Yaël Dillies]

I think not

[Yury G. Kudryashov]

But I would prefer to hear from people who work on core and on Lean 4 migration.

[Yury G. Kudryashov]

I think that the correct question is: will we ever need an instance of has_ssubset that is not defeq to "subset and not subset".

[Kevin Buzzard]

Do we have many instances of lt which are not defeq to le_and_not_le?

[Yaël Dillies]

Lots. Notably, every time you make <= and < primitive on a new type, eg docs#sum.has_lt, docs#sigma
has_lt, docs#sum.lex.has_lt, docs#sigma.lex.has_lt. There's also docs#finset.colex whose < is primitive and <= derived.

[Kevin Buzzard]

Oh -- I had imagined that people would in practice be using the autoparam to fill in the field in preorder

[Yaël Dillies]

They do, but only when you can't lift < itself.

[Yury G. Kudryashov]

See also docs#complex.partial_order

[Anne Baanen]

For what it's worth, instance does nothing with out_params: the elaborator checks for out_param in the class before the first instance of a search is tried. (And I should have fixed out_param instance parameters in one of the lean 3.35-3.37 releases, so that β : out_param Type implies that has_mem β α is effectively also an out_param.) So since docs#has_mem already has β as out_param, we can just write:

instance {α : Type*} {β : Type*} [has_mem β α] : has_subset α :=
⟨λ s t, ∀ {{x : β}}, x ∈ s → x ∈ t⟩

[Anne Baanen]

I would replace the has_mem constraint with set_like instead, since docs#set_like.partial_order already provides the correct definition for ≤ and makes < defeq to ≤ and not ≥.

[Anne Baanen]

So my proposal:

instance {α : Type*} {β : Type*} [set_like β α] : has_subset α :=
⟨(≤)⟩

instance {α : Type*} {β : Type*} [set_like β α] : has_ssubset α :=
⟨(<)⟩

[Yury G. Kudryashov]

These instances don't work, e.g., for lists.

[Yaël Dillies]

Nor multiset

[Anne Baanen]

Those can still have their own instances, no?

[Yury G. Kudryashov]

My idea was to either unify all instances of has_subset/has_ssubset, or to replace them with defs.

[Yury G. Kudryashov]

BTW, does it make sense to have set_like (set α)?

[Yury G. Kudryashov]

I mean, will it create any strange instances?

[Anne Baanen]

Yury G. Kudryashov said:

My idea was to either unify all instances of has_subset/has_ssubset, or to replace them with defs.

I see, then your proposal also looks good to me!

[Anne Baanen]

Yury G. Kudryashov said:

BTW, does it make sense to have set_like (set α)?

If it's like fun_like (α → β), then it might insert some unnecessary coe : set α → set α. Otherwise I didn't see any real weirdnesses.

[Yury G. Kudryashov]

/poll What should we do with has_subset/has_ssubset?
Leave them as is
Add generic instances and use them instead of type-specific ones
Replace with defs

[Yaël Dillies]

Actually, couldn't we generalize even more and allow an heterogenous subset?

def subset {α β γ : Type*} [has_mem α β] [has_mem α γ] (s : β) (t : γ) : Prop :=
∀ ⦃x : α⦄, x ∈ s → x ∈ t

[Yaël Dillies]

Doing so, we wouldn't have to rely on the coercion to sets to compare finsets and lists, for example.

[Yaël Dillies]

Is docs#has_subset used anywhere in core Lean?

[Eric Wieser]

I get the feeling making it heterogenous would be a bad idea

[Eric Wieser]

As then things like docs#set.finite.subset wouldn't obviously apply if one of your sets is a finset

[Yaël Dillies]

What does set.finite.subset have to do with anything? This statement wouldn't change, right?

[Eric Wieser]

Sure the statement would be the same, but the hypothesis would be harder to satisfy

[Eric Wieser]

As now someone would have likely have fs ⊆ s, but need to produce (↑fs : set _) ⊆ s to apply the lemma. They're probably defeq, but I don't think library_search will know that.

[Eric Wieser]

My point is that probably all useful lemmas will be stated about the homogenous version, and so the heterogeneous version will just be harder to work with for little benefit