Zulip Chat Archive

Stream: general

Topic: has_mem disjoint


view this post on Zulip Sean Leather (Oct 02 2018 at 06:38):

Currently, there is this definition in data/list/basic.lean:

def disjoint (l₁ l₂ : list α) : Prop :=
 a⦄, a  l₁  a  l₂

Would there be any interest in replacing it with the following more general version?

def disjoint {α β₁ β₂} [has_mem α β₁] [has_mem α β₂] (b₁ : β₁) (b₂ : β₂) : Prop :=
 a : α⦄, a  b₁  a  b₂

I'm using the latter quite a lot, and a number of the list theorems can be stated about it instead.

view this post on Zulip Simon Hudon (Oct 02 2018 at 06:40):

Can those list theorems be generalized too?

view this post on Zulip Sean Leather (Oct 02 2018 at 06:40):

A number of them could.

view this post on Zulip Simon Hudon (Oct 02 2018 at 06:41):

What assumptions do they need on top of has_mem?

view this post on Zulip Sean Leather (Oct 02 2018 at 06:42):

I haven't looked into it, but theorems like this obviously need lists:

theorem disjoint_of_disjoint_cons_left {a : α} {l₁ l₂} : disjoint (a::l₁) l₂  disjoint l₁ l₂

view this post on Zulip Sean Leather (Oct 02 2018 at 06:43):

But this...

theorem disjoint.symm {l₁ l₂ : list α} (d : disjoint l₁ l₂) : disjoint l₂ l₁
| a i₂ i₁ := d i₁ i₂

view this post on Zulip Kenny Lau (Oct 02 2018 at 06:44):

you mean lattice.disjoint

view this post on Zulip Simon Hudon (Oct 02 2018 at 06:44):

I guess you could also reformulate the first one to use insert

view this post on Zulip Sean Leather (Oct 02 2018 at 06:44):

For me, the latter disjoint is useful when mixing list and finset.

view this post on Zulip Sean Leather (Oct 02 2018 at 06:45):

you mean lattice.disjoint

I don't think I do. I specifically want has_mem.

view this post on Zulip Kenny Lau (Oct 02 2018 at 06:45):

but what structure has mem?

view this post on Zulip Sean Leather (Oct 02 2018 at 06:45):

Also, β₁ and β₂ are different.

view this post on Zulip Kenny Lau (Oct 02 2018 at 06:45):

does this make much sense for option.has_mem?

view this post on Zulip Sean Leather (Oct 02 2018 at 06:46):

I guess you could also reformulate the first one to use insert

I don't think you want to do that. It's a useful theorem by its own right.

view this post on Zulip Simon Hudon (Oct 02 2018 at 06:46):

Right, I would keep both

view this post on Zulip Sean Leather (Oct 02 2018 at 06:51):

Kenny: I don't understand what you mean. Plenty of things have has_mem instances:

category_theory/examples/topological_spaces.lean:instance : has_mem X.α (open_set X) :=
computability/partrec_code.lean:instance : has_mem ( →. ) code := ⟨λ f c, eval c = f
data/finset.lean:instance : has_mem α (finset α) := ⟨λ a s, a  s.1
data/hash_map.lean:instance : has_mem α (hash_map α β) := ⟨λa m, m.contains a
data/multiset.lean:instance : has_mem α (multiset α) := mem
data/option.lean:instance has_mem : has_mem α (option α) := ⟨λ a b, b = some a
data/pfun.lean:instance : has_mem α (roption α) := roption.mem
data/semiquot.lean:instance : has_mem α (semiquot α) := ⟨λ a q, a  q.s
data/seq/computation.lean:instance : has_mem α (computation α) := computation.mem
data/seq/seq.lean:instance : has_mem α (seq α) :=
data/seq/wseq.lean:instance : has_mem α (wseq α) :=
data/seq/wseq.lean:    unfold cons has_mem.mem wseq.mem seq.mem seq.cons, simp,
linear_algebra/submodule.lean:instance : has_mem β (submodule α β) := ⟨λ x y, x  (y : set β)
logic/basic.lean:theorem ne_of_mem_of_not_mem {α β} [has_mem α β] {s : β} {a b : α}
set_theory/lists.lean:instance {b} : has_mem (lists α) (lists' α b) :=
set_theory/lists.lean:instance : has_mem (lists α) (lists α) := mem
set_theory/zfc.lean:instance : has_mem pSet.{u} pSet.{u} := mem
set_theory/zfc.lean:instance : has_mem Set Set := mem
set_theory/zfc.lean:show @has_mem.mem _ _ Set.has_mem y α, A  p y, from
set_theory/zfc.lean:instance : has_mem Class Class := Class.mem

view this post on Zulip Kenny Lau (Oct 02 2018 at 07:13):

how did you search that?

view this post on Zulip Kenny Lau (Oct 02 2018 at 07:14):

oh, it's a grep right

view this post on Zulip Sean Leather (Oct 02 2018 at 07:23):

how did you search that?

git grep has_mem

view this post on Zulip Simon Hudon (Oct 02 2018 at 07:25):

Why not #print instances has_mem?

view this post on Zulip Sean Leather (Oct 02 2018 at 07:27):

Why not? You could use that, too. git grep is faster and, in this case, useful enough.

view this post on Zulip Simon Hudon (Oct 02 2018 at 07:28):

I accept your answer.

view this post on Zulip Johannes Hölzl (Oct 02 2018 at 07:37):

I don't think a has_mem version of disjoint makes sense. You get surely some basic facts from the implication. But otherwise we don't have any structure behind mem. Its better to use the lattice version.

view this post on Zulip Sean Leather (Oct 02 2018 at 07:39):

In my case (which may be strange), I can't use the lattice version. It requires the types to be the same.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 07:39):

Note that anything that satisfies that definition also fits the lattice definition (at least mathematically), since it can be expressed on the lattice of sets {x | x \in s}

view this post on Zulip Sean Leather (Oct 02 2018 at 07:40):

In particular, I want to show that a list and a finset are disjoint.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 07:40):

oh, I see you've made the types different

view this post on Zulip Mario Carneiro (Oct 02 2018 at 07:40):

just say l1.to_finset.disjoint s2

view this post on Zulip Sean Leather (Oct 02 2018 at 07:40):

just say l1.to_finset.disjoint s2

That adds the extra baggage of to_finset, which I don't need.

view this post on Zulip Sean Leather (Oct 02 2018 at 07:41):

I really just want ∀ ⦃a : α⦄, a ∈ b₁ → a ∉ b₂.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 07:42):

then define it for yourself

view this post on Zulip Mario Carneiro (Oct 02 2018 at 07:43):

I don't see strong evidence that this is a common case

view this post on Zulip Sean Leather (Oct 02 2018 at 08:11):

I don't think a has_mem version of disjoint makes sense. You get surely some basic facts from the implication. But otherwise we don't have any structure behind mem.

Just to make my final case for the has_mem-based disjoint above before I go away. :slight_smile:

Advantages:

1. It provides a nice generalization of the list-based disjoint. So, you can define the basic implication facts such that they work for other types beside list. And, yet, you can also define the list disjoint facts just as they are, so you don't lose anything.
2. It works with two different types, while the lattice disjoint doesn't.
3. Useful simplification theorems can be defined for different combinations of types.

Disadvantages:

1. It adds too much generality?

(I'm having trouble thinking of disadvantages.)

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:13):

can you do the lattice disjoint using has_mem disjoint?

view this post on Zulip Sean Leather (Oct 02 2018 at 08:14):

can you do the lattice disjoint using has_mem disjoint?

What do you mean?

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:14):

you say it's more general, but it doesn't capture the generality of lattices

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:14):

so it's really just a generalization in a different direction

view this post on Zulip Sean Leather (Oct 02 2018 at 08:15):

More general in the sense that the “sets” are different even though the element type is the same.

view this post on Zulip Sean Leather (Oct 02 2018 at 08:15):

so it's really just a generalization in a different direction

Yes.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:15):

In particular, I like that the bottom element need not be the empty set / "false"

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:16):

i.e. when I am talking about disjoint subgroups

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:17):

This kind of generality gets use in several places in mathlib. Multiple type disjointness does not

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:17):

If it comes up, I'm prepared to consider a definition but we have zero theorems that need this right now

view this post on Zulip Sean Leather (Oct 02 2018 at 08:17):

Yeah, so this is not a very mathematically elegant generality, more of a practical one. :slight_smile:

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:18):

if all the theorems are in your project, then so should this definition

view this post on Zulip Mario Carneiro (Oct 02 2018 at 08:19):

I'm not saying it's a bad definition, but it is certainly "premature optimization" for mathlib

view this post on Zulip Sean Leather (Oct 02 2018 at 08:20):

That may be.

view this post on Zulip Simon Hudon (Oct 02 2018 at 19:23):

You could have a function to_set [has_mem a b] : b -> set a for which @Sean Leather' version of disjoint is consistent with to_set a ∩ to_set b = ∅ even if a and b have different types.


Last updated: May 12 2021 at 23:13 UTC