decidable disjoint

Stream: new members

[Bhavik Mehta]

When I write:

import data.finset
import data.fintype

open fintype
open finset

variable {n : ℕ}
local notation `X` := fin n

variable {𝒜 : finset (finset X)}

def compress (U V : finset X) (A : finset X) :=
if (disjoint U A) ∧ (V ⊆ A)
  then (A ∪ U) \ V
  else A

I get an error saying "failed to synthesize type class instance" for "decidable (disjoint U A ∧ V ⊆ A)", but if I rewrite the condition with U ∩ A = ∅, it's fine... I'd like to keep the definition with disjoint though, since every time I use this definition I found myself converting the empty intersection to disjointness. How could I get around this?

[Bhavik Mehta]

I proved disjoint U V is decidable instead... Is there a reason this isn't already in data/finset.lean?

[Simon Hudon]

There's no reason not to have it in mathlib. People tend to add what they use so that might just never have come up before

[Bhavik Mehta]

Okay! Is there an issue with typeclass resolution, since this is saying disjoint on finsets is decidable, but might not be in other cases?

[Simon Hudon]

With decidable equality on α, disjointness on finset should always be decidable.