Dot notation for ⊆ and ⊂

Stream: general

[Yaël Dillies]

We currently have no dot notation relating ⊆ and ⊂ because we have no analog of preorder for them. This is very annoying because then you have lemmas like docs#finset.ssubset_of_subset_of_ssubset which take ages to write down. I'm thinking of defining such a thing. Given that it's only used by set and finset, an unbundled relation class should be enough while easy and lightweight.

Are people against the idea? If not, how should it be called? is_preorder is already taken.

[Anne Baanen]

ordered_set_like?

[Yaël Dillies]

I was thinking of a more general class

class TBD (α : Type*) (r s : α → α → Prop) extends is_preorder α r :=
(right_iff_left_not_left {a b : α} : s a b ↔ r a b ∧ ¬ r b a)

[Yaël Dillies]

Or maybe just

class TBD (α : Type*) (r s : α → α → Prop) :=
(right_iff_left_not_left {a b : α} : s a b ↔ r a b ∧ ¬ r b a)

because we're really only needing the interaction. Existing typeclasses already handle each of ⊆ and ⊂ alone

[Anne Baanen]

I see! So assuming a name like strict_nonstrict_order, the actual dot-notated lemmas you want look like:

lemma has_ssubset.ssubset.subset {S : Type*} [has_subset S] [has_ssubset S] [strict_nonstrict_order (⊆) (⊂)]
  {a b : S} (h : a ⊂ b) : a ⊆ b := _

Right?

[Yaël Dillies]

Yes, exactly!

[Anne Baanen]

I would definitely remove the extends since you'll get a dangerous instance.

[Eric Wieser]

Yaël Dillies said:

I was thinking of a more general class

class TBD (α : Type*) (r s : α → α → Prop) extends is_preorder α r :=
(right_iff_left_not_left {a b : α} : s a b ↔ r a b ∧ ¬ r b a)

The TBD.to_is_preorder this creates is dangerous as is has no way to infer s. So your other suggestion is the right one

[Yaël Dillies]

I definitely the extends too :grinning:

[Eric Wieser]

I also definitely the extends, simultaneously it seems

[Yaël Dillies]

#11381