has_mem disjoint

Stream: general

[Sean Leather]

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]

Can those list theorems be generalized too?

[Sean Leather]

A number of them could.

[Simon Hudon]

What assumptions do they need on top of has_mem?

[Sean Leather]

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₂

[Sean Leather]

But this...

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

[Kenny Lau]

you mean lattice.disjoint

[Simon Hudon]

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

[Sean Leather]

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

[Sean Leather]

you mean lattice.disjoint

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

[Kenny Lau]

but what structure has mem?

[Sean Leather]

Also, β₁ and β₂ are different.

[Kenny Lau]

does this make much sense for option.has_mem?

[Sean Leather]

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]

Right, I would keep both

[Sean Leather]

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]

how did you search that?

[Kenny Lau]

oh, it's a grep right

[Sean Leather]

how did you search that?

git grep has_mem

[Simon Hudon]

Why not #print instances has_mem?

[Sean Leather]

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

[Simon Hudon]

I accept your answer.

[Johannes Hölzl]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

oh, I see you've made the types different

[Mario Carneiro]

just say l1.to_finset.disjoint s2

[Sean Leather]

just say l1.to_finset.disjoint s2

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

[Sean Leather]

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

[Mario Carneiro]

then define it for yourself

[Mario Carneiro]

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

[Sean Leather]

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]

can you do the lattice disjoint using has_mem disjoint?

[Sean Leather]

can you do the lattice disjoint using has_mem disjoint?

What do you mean?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

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

[Sean Leather]

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

Yes.

[Mario Carneiro]

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

[Mario Carneiro]

i.e. when I am talking about disjoint subgroups

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

That may be.

[Simon Hudon]

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.