Capricious dot notation

Stream: general

[Yaël Dillies]

I'm having many problems with dot notation for stuff like .trans and antisymm. Did anything change fairly recently?
For example

example {E : Type u_1}
  [add_comm_group E]
  [module ℝ E]
  {A B : set E}
  (hA : ∀ ⦃x y : E⦄, x ∈ A → y ∈ A → open_segment x y ⊆ A)
  ⦃x y : E⦄
  (hx : x ∈ A)
  (hy : y ∈ A) :
  open_segment x y ⊆ convex_join A B :=
begin
  exact (hA hx hy).trans (subset_convex_join_left A B),
  --fails while `hA hx hy : open_segment x y ⊆ A` and `subset_convex_join_left A B : A ⊆ convex_join A B`
end

The exact error is invalid field notation, insufficient number of arguments for 'set.subset.trans'.

[Yaël Dillies]

And exact subset.trans (hA hx hy) (subset_convex_join_left A B), works just fine.

[Patrick Massot]

This cannot work because the lemma is not in the right namespace

[Patrick Massot]

I would be in favor of adding

import data.set.basic

lemma has_subset.subset.trans {α : Type*} {a b c : set α} (h : a ⊆ b)  (h': b ⊆ c) :
  a ⊆ c := set.subset.trans h h'

example {α : Type*} {a b c : set α} (h : a ⊆ b)  (h': b ⊆ c) : a ⊆ c :=
h.trans h'

[Patrick Massot]

If nobody complains soon then I'll open a PR

[Patrick Massot]

And I don't think anything changed recently here. And dot notation isn't capricious here, it's behaving entirely according to spec

[Yaël Dillies]

I swear this was working a few days ago.

[Yaël Dillies]

Or maybe my use case changed in the last few days :thinking:

[Patrick Massot]

The reason why people may complain is that set X is not the only instance of has_subset, see docs#has_subset, but I don't know what typeclasses we could use here to say that whatever the subset notation denotes is transitive (or antisymmetric).

[Patrick Massot]

We could had a typeclass has_lawful_subset, but I suspect it wouldn't be worth the trouble since set is probably overwhelmingly more relevant (except maybe over finset)

[Patrick Massot]

@Mario Carneiro any input here?

[Mario Carneiro]

Your definition seems fine to me

[Mario Carneiro]

we already have something like that for src#has_le.le.trans

[Mario Carneiro]

I wouldn't worry too much about subset being a more general typeclass; we overwhelmingly prefer le for other subset-like things (and I think @Kevin Buzzard has proposed using le also for sets)

[Eric Wieser]

I think finset alone makes adding the lawful typeclass worthwhile

[Kevin Buzzard]

People have seemed to argue that we shouldn't pander to the undergraduates and have vector_space when all us grown-ups know that this just means module. The only purpose of $\subseteq$ is to be a special-case notation for $\le$ for historical reasons, so exactly the same arguments seem to apply to me.

[Gabriel Ebner]

Patrick Massot said:

We could had a typeclass has_lawful_subset, but I suspect it wouldn't be worth the trouble since set is probably overwhelmingly more relevant (except maybe over finset)

We already have a typeclass called is_trans that I would use for has_subset.subset.trans. (which allows you to write trans x y for lots of x and ys)

[Eric Wieser]

What instances does docs#is_trans already have?

[Eric Wieser]

I guess is_preorder (has_subset.subset : set a -> set a -> Prop) is the missing instance?

[Patrick Massot]

#7681

[Sebastien Gouezel]

The PR only records the instance on sets, not finsets. Was it already registered on finsets?

[Patrick Massot]

It's not needed, I guess it's because finset subset is defeq to set finset

[Eric Wieser]

I think both instances already exist: this works fine on master:

example {α : Type*} : is_trans (set α) set.subset := by show_term {apply_instance}
example {α : Type*} : is_trans (set α) (⊆) := by show_term {apply_instance}
example {α : Type*} : is_trans (finset α) (⊆) := by show_term {apply_instance}

[Patrick Massot]

Oh great! Only the two lemmas were missing then

[Patrick Massot]

fixed

[Eric Wieser]

Do we want this one too?

-- TODO: do we have this somewhere?
lemma irrefl_ne {α : Type*} {r : α → α → Prop} [is_irrefl α r] : ∀ {a b} (h : r a b), a ≠ b
| a b h rfl := irrefl _ h

lemma has_ssubset.ssubset.ne {α : Type*} [has_ssubset α] [is_irrefl α (⊂)]
  {a b : α} (h : a ⊂ b) : a ≠ b := irrefl_ne h

[Patrick Massot]

I never use ⊂, but why not?

[Yaël Dillies]

Thanks a lot for the PR!