TODO: unify disjoint

[johoelzl]

Introduce disjoint on has_mem and unify the list, multiset, finset instances. The finset instance would be generalized by removing the requirement for decidable_eq

[spl]

Just curious what your idea is. This would be a different definition from the root disjoint in data/set/lattice.lean?

def disjoint (a b : α) : Prop := a ⊓ b = ⊥

Would you define something like this?

def disjoint [has_mem α γ] (s t : γ) : Prop := ∀ ⦃a : α⦄, a ∈ s → a ∈ t → false

How does this affect the finset disjoint?

[digama0]

I changed the definition of disjoint in my local copy to s \cap t <= \bot, which works much better with existing definitions in list and multiset and set. I'll push it soonish and then we can fiddle some more if it's still not working well.

[johoelzl]

It would generalize disjoint on finset, as it would require anymore decidable_eq

[semorrison]

@digama0, did you ever push your change mentioned above?

[jcommelin]

@digama0, did you ever push your change mentioned above?

[eric-wieser]

@digama0 pushed the change mentioned above in bdc90f6#diff-fcfc782476bb085e78399cffbe5ef17d89cac39446fa8e27de27224019d0f7acR532

[eric-wieser]

Perhaps we should leave this open as a "document why we use ≤ in the definition" issue