mem_of_super_set

Stream: general

[Patrick Massot]

This time I ask before refactoring: should we add

import order.filter.basic

open filter

lemma has_mem.mem.up {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
mem_of_superset hx h

example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
hx.up h

If yes, what would be a good name? up is very short, but is it clear enough?

[Patrick Massot]

This lemma is used a lot.

[Eric Wieser]

It feels a bit weird to put dot notation on has_mem.mem that only applies to one particular instance of has_mem

[Eric Wieser]

Here's a neat trick that doesn't prevent other types defining a different meaning of has_mem.up:

import order.filter.basic

open filter

/-- Alias for dot notation -/
abbreviation filter_mem_dot_notation (P : Prop) : Prop := P

-- wrap the resulting `Prop` in a type alias for dot notation
instance filter.has_mem' {α : Type*} : has_mem (set α) (filter α) :=
{mem := λ u f, filter_mem_dot_notation (u ∈ f.sets) }

--note: for dot notation, `hx` is wrapped.
lemma filter_mem_dot_notation.up {α : Type*} {f : filter α} {x y : set α}
  (hx : filter_mem_dot_notation (x ∈ f)) (h : x ⊆ y) : y ∈ f :=
sorry

-- result: dot notation that is specific to `filter.has_mem`
example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
hx.up h

(edit: split the discussion about error message weirdness to a new thread)

[Patrick Massot]

This weirdness is the reason why it wasn't done before, but it actually causes no harm (and I think we recently did the same for other similar cases).

[Eric Wieser]

I'm not sure I understand; are you saying that your original has_mem.mem.up causes no harm, or that my revised solution that doesn't produce the weird error causes no harm?

[Patrick Massot]

I'm talking about my suggestion.

[Patrick Massot]

But if yours works and does not leak anywhere then it's ok.

[Eric Wieser]

Just checking you weren't saying that we'd already used the trick I suggest elsewhere. Can you come up with a similar case for the approach you suggest? It might be worth assembling a list of things like has_mem.mem.up, so that in future someone can try the dot notation hack I suggest above in lots of places at once, in order to increase the chance of finding leaks.

[Patrick Massot]

Sorry, I need to go now. I'll return tonight.

[Kyle Miller]

Would it still work if it were put on has_subset.subset instead? I like thinking of this fact as being functorial in h.

lemma has_subset.subset.up {α : Type*} {f : filter α} {x y : set α} (h : x ⊆ y) (hx : x ∈ f) : y ∈ f

To make this more general, there could be a typeclass to introduce has_subset.subset.up functors:

import order.filter.basic

open filter

class has_subset_up (α : Type*) [has_subset α] (β : α → Sort*) :=
(up : Π {x y : α}, x ⊆ y → β x → β y)

lemma has_subset.subset.up {α : Type*} [has_subset α] {β : α → Sort*} [has_subset_up α β]
  {x y : α}
  (h : x ⊆ y) (hx : β x) : β y :=
has_subset_up.up h hx

instance filter.subset_up {α : Type*} (f : filter α) : has_subset_up (set α) (∈f) :=
{ up := λ x y h hx, mem_of_superset hx h }

example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
h.up hx

Or there could be a more specialized version of this:

import order.filter.basic

open filter

class has_subset_up (α : out_param $ Type*) (β : Type*) [has_mem α β] [has_subset α] :=
(up : ∀ {x y : α} {z : β}, x ⊆ y → x ∈ z → y ∈ z)

lemma has_subset.subset.up {α : Type*} {β : Type*} [has_mem α β] [has_subset α] [has_subset_up α β]
  {x y : α} {z : β}
  (h : x ⊆ y) (hx : x ∈ z) : y ∈ z :=
has_subset_up.up h hx

instance {α : Type*} : has_subset_up (set α) (filter α) :=
{ up := λ x y z h hx, mem_of_superset hx h }

example {α : Type*} {f : filter α} {x y : set α} (hx : x ∈ f) (h : x ⊆ y) : y ∈ f :=
h.up hx

[Eric Wieser]

The typeclass approach is probably more sensible than the type alias approach I suggested. Can you think of a second instance, or is the only place this happens on filters anyway?

[Kyle Miller]

instance subtype.subset_up {α : Type*} : has_subset_up (set α) (λ s, s) :=
{ up := λ x y, set.inclusion }

example {α : Type*} (x y : set α) (h : x ⊆ y) (a : x) : y := h.up a

[Kyle Miller]

I can't get it to work where up gives structured functions, like homomorphisms. The subset relation for subobjects giving homomorphisms between their coercions to types could have been another use.

[Kyle Miller]

What I tried was

class has_subset_up (α : Type*) [has_subset α] (β : α → α → Sort*) :=
(up : Π {x y : α}, x ⊆ y → β x y)

but then h.up a is "too many arguments"

[Eric Wieser]

β should be an outparam, right?

[Kyle Miller]

Do you mean in this version?

class has_subset_up (α : Type*) [has_subset α] (β : α → Sort*) :=
(up : Π {x y : α}, x ⊆ y → β x → β y)

It's not an out_param because subset-of relations can have multiple induced maps. set α can have one for both filter and subtype.

[Patrick Massot]

All this is a lot of fun but it really smells over-engineering until we have a second lemma that would use it.

[Patrick Massot]

My original suggestion works without any type class search or tricky aliasing.

[Kyle Miller]

@Patrick Massot Is there any reason the filter lemma couldn't be has_subset.subset.up? Another possible name is has_subset.subset.map, though I don't think there's much of a reason to prefer that over up.

[Patrick Massot]

I don't care about attaching it to has_mem vs has_subset, both would make sense.