set.nontrivial

Stream: maths

[Wrenna Robson]

I am considering the benefits of a set.nontrivial predicate, with the property that s.nontrivial iff ¬ s.subsingleton. This would allow for the use of dot notation etc. This is analogous to the subsingleton and nontrivial typeclasses. What are people's thoughts?

[Wrenna Robson]

(This comes up naturally when considering things like the infimum distance of a set under a metric.)

[Kyle Miller]

Would writing ¬ s.subsingleton be sufficient? Or would you be wanting to have lemmas you access via dot notation on a set.nontrivial term?

[Kyle Miller]

I think the reason a special nontrivial class exists is that typeclass inference wouldn't really work for ¬ (subsingleton X).

[Wrenna Robson]

I had been writing ¬ s.subsingleton, but, exactly as you say, I kept wanting a dot notation for it.

(Also I would define s.nontrivial as the push_neg version, i.e. not "not forall" but "exists" - bit easier to actually use.)

[Violeta Hernández]

Wrenna Robson said:

I am considering the benefits of a set.nontrivial predicate, with the property that s.nontrivial iff ¬ s.subsingleton. This would allow for the use of dot notation etc. This is analogous to the subsingleton and nontrivial typeclasses. What are people's thoughts?

Given that we already have quite a few set analogs of typeclasses, such as set.nonempty, set.subsingleton, set.finite, set.infinite, set.countable, I think one more will be welcome as long as it has the appropriate API

[Kyle Miller]

Dot notation seems to be sufficient cause for a special predicate. I think it's fair define it in the most convenient form, then prove it's equivalent to ¬ s.subsingleton (I assume they're literally push_negs of each other.)

You'll still need to create API to link up nontrivial and set.nontrivial (and rename any not_subsingleton lemmas), but maybe some of that already exists.

[Violeta Hernández]

I'd say the "correct" definition of set.nontrivial is the one that matches nontrivial, which is ∃ x y ∈ s, x ≠ y

[Kyle Miller]

(Yes, that's the push-neg of the negation of docs#set.subsingleton)

[Violeta Hernández]

The simp-normal form of ¬ s.subsingleton should be made into s.nontrivial, and you should also have a lemma set.nontrivial_coe_iff : nontrivial (↥s) ↔ s.nontrivial.

[Kyle Miller]

Dot notation seems to be sufficient cause for a special predicate.

I've thought about an extension to dot notation that would help us out here, but there are still some details I'm not sure about, and like always Lean 4 is around the corner so it's not the best idea to put energy into this.

The idea is that when doing dot notation lookup for x.foo when x : a (b ...) you would first look for a.foo and then if that fails you would look for b.a.foo. It'd only go looking this far, not recursively.

Then you could have set.subsingleton.not lemmas.

[Kyle Miller]

One place this is not the best is with has_mem lemmas. When you have h : x ∈ s and s : a, ideally h.foo would look at a.has_mem.mem.foo. With my simpler idea, it only would look for a lemma associated to x.

[Wrenna Robson]

Do we have such a coe_iff lemma for subsingleton?

[Yaël Dillies]

docs#set.subsingleton_coe

[Wrenna Robson]

Right. My plan was to essentially mirror all the API for set.subsingleton. I don't think we have many not_subsingleton lemmas but they might be called something different.

[Wrenna Robson]

(...arguably you could have a similar pair of predicates for finset...)

[Yaël Dillies]

Actually we don't even have finset.subsingleton.

[Wrenna Robson]

Right.

[Wrenna Robson]

Is there a need for it? I can see that it might come up.

[Wrenna Robson]

Is there a need for it? I can see that it might come up.

[Violeta Hernández]

My take on API is to add it only when it's either relevant or trivial

[Violeta Hernández]

If we don't need finset.singleton yet, no need to add the API

[Violeta Hernández]

At the end of the day, it's the theorems you use the API on that inform how it should look, not the other way around

[Wrenna Robson]

Well, I do have a need for it... but it might just be me.

[Wrenna Robson]

incidentally, set.nontrivial is currently the name of the nontrivial instance of set.

[Wrenna Robson]

Could rename to nontrivial_of_nonempty or something

[Wrenna Robson]

What do you think?

[Kyle Miller]

Renaming the instance seems fine to me. docs#set.nontrivial is the fact that set X itself is nontrivial -- I wonder if something like nontrivial_set is a more appropriate name? I'm not sure.

docs#set.nontrivial_mono might want to be renamed too (or replaced with a set.nontrivial version?)

[Yaël Dillies]

No because we will call the set.nontrivial version set.nontrivial.mono.

[Wrenna Robson]

#15867 now exists

[Wrenna Robson]

(I kept nontrivial_mono, though I moved it later in the file to take advantage of the new functionality.)

[Wrenna Robson]

I've made a couple of additions and changes to subsingleton, but they were really only things that I noticed as I was going, I've tried to keep to a fairly tight scope.

[Wrenna Robson]

And I finally got it to build...!