Set predicates and set-like.

Stream: maths

[Wrenna Robson]

We have a number of predicates: set.nonempty, set.nontrivial, set.subsingleton (and arguably you could have set.empty also, though that's a bit odd) which have analogous concepts in finset, but for which we only have finset.nonempty (the other two being newer). I could just add them. However, it strikes me that really these are somehow "the same" as the set ones - and I was wondering if there's a typeclass solution.

Now finset doesn't have a set_like instance, though there's an argument it could. If it did, would it be worth defining these predicates on set_like? Would you then be able to use dot notation in the expected way?

It's just an idle idea - the easiest thing is just to create a copy in finset. But it is a mild pain making sure that such things are done: surely we have the technology to automate it somewhat?

[Kyle Miller]

I've suggested one potential feature in issue lean4#1629 that could be used to support these predicates with dot notation. If something like that makes it into Lean 4, then it wouldn't be too hard to backport it to Lean 3.

Note that all these predicates don't depend on anything more than has_mem, which is good since from what I remember people have had trouble making set be set_like.

[Wrenna Robson]

That's true, actually - they possibly in fact should just be dependent on has_mem.

[Wrenna Robson]

Your feature idea is interesting.