# Zulip Chat Archive

## Stream: general

### Topic: has_mem disjoint

#### 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.

#### Simon Hudon (Oct 02 2018 at 06:40):

Can those list theorems be generalized too?

#### Sean Leather (Oct 02 2018 at 06:40):

A number of them could.

#### Simon Hudon (Oct 02 2018 at 06:41):

What assumptions do they need on top of `has_mem`

?

#### Sean Leather (Oct 02 2018 at 06:42):

I haven't looked into it, but theorems like this obviously need `list`

s:

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

#### 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₂

#### Kenny Lau (Oct 02 2018 at 06:44):

you mean `lattice.disjoint`

#### Simon Hudon (Oct 02 2018 at 06:44):

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

#### Sean Leather (Oct 02 2018 at 06:44):

For me, the latter `disjoint`

is useful when mixing `list`

and `finset`

.

#### Sean Leather (Oct 02 2018 at 06:45):

you mean

`lattice.disjoint`

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

.

#### Kenny Lau (Oct 02 2018 at 06:45):

but what structure has mem?

#### Sean Leather (Oct 02 2018 at 06:45):

Also, `β₁`

and `β₂`

are different.

#### Kenny Lau (Oct 02 2018 at 06:45):

does this make much sense for `option.has_mem`

?

#### 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.

#### Simon Hudon (Oct 02 2018 at 06:46):

Right, I would keep both

#### 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⟩

#### Kenny Lau (Oct 02 2018 at 07:13):

how did you search that?

#### Kenny Lau (Oct 02 2018 at 07:14):

oh, it's a grep right

#### Sean Leather (Oct 02 2018 at 07:23):

how did you search that?

`git grep has_mem`

#### Simon Hudon (Oct 02 2018 at 07:25):

Why not `#print instances has_mem`

?

#### 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.

#### Simon Hudon (Oct 02 2018 at 07:28):

I accept your answer.

#### 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.

#### 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.

#### 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}`

#### Sean Leather (Oct 02 2018 at 07:40):

In particular, I want to show that a `list`

and a `finset`

are disjoint.

#### Mario Carneiro (Oct 02 2018 at 07:40):

oh, I see you've made the types different

#### Mario Carneiro (Oct 02 2018 at 07:40):

just say `l1.to_finset.disjoint s2`

#### 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.

#### Sean Leather (Oct 02 2018 at 07:41):

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

.

#### Mario Carneiro (Oct 02 2018 at 07:42):

then define it for yourself

#### Mario Carneiro (Oct 02 2018 at 07:43):

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

#### 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.)

#### Mario Carneiro (Oct 02 2018 at 08:13):

can you do the lattice disjoint using has_mem disjoint?

#### Sean Leather (Oct 02 2018 at 08:14):

can you do the lattice disjoint using has_mem disjoint?

What do you mean?

#### Mario Carneiro (Oct 02 2018 at 08:14):

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

#### Mario Carneiro (Oct 02 2018 at 08:14):

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

#### 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.

#### Sean Leather (Oct 02 2018 at 08:15):

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

Yes.

#### Mario Carneiro (Oct 02 2018 at 08:15):

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

#### Mario Carneiro (Oct 02 2018 at 08:16):

i.e. when I am talking about disjoint subgroups

#### Mario Carneiro (Oct 02 2018 at 08:17):

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

#### 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

#### 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:

#### Mario Carneiro (Oct 02 2018 at 08:18):

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

#### 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

#### Sean Leather (Oct 02 2018 at 08:20):

That may be.

#### 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