Failed to synthesize Decidable

Stream: new members

[Björn Wehlin]

I'm having some issue with sets that I can't quite untangle. See the following code:

theorem dsaasd {E : Type*} [MeasurableSpace E]
    (ι : Type*) [Countable ι] (f : ι → E) (s : Set E) :
    ∀ i : ι, (dirac (f i)) s = (if (f i) ∈ s then 1 else 0) := by

  let t := { i | f i ∈ s }
  sorry

For some reason, in the theorem statement, Lean complains that failed to synthesize Decidable (f i ∈ s), whereas let t := { i | f i ∈ s } is OK. What am I doing wrong here? Thanks!

[Eric Wieser]

The fix here is to add [DecidablePred (· ∈ s)]

[Eric Wieser]

You don't need it for {i | f i ∈ s} because that's just a set literal, not a decision procedure like if.

[Björn Wehlin]

Doesn't that just bump the issue one level up in that I would then have to supply the decidability when I use the theorem? (Is there some formal reason why I can't assume that I can ask the question "is f i an element of the set s"?)

[Eric Wieser]

Sure, but when you use the theorem you can just write classical in the proof and it's fine

[Eric Wieser]

You only should add these assumptions when the statement requires them, because if you don't then the thing you proved isn't as general as it might need to be

[Björn Wehlin]

Aha, I had seen classical floating around in various places without knowing what it does. From what I can glean from the Mathlib code, all classical does is makes set belonging decidable. Is this correct? If so, I think it's probably OK for what I'm doing now.

[Aaron Liu]

The problem is if you have a concrete set whose membership is decidable (like Set.Ico 0 1) and you decide to use classical in the theorem statement instead of [DecidablePred (· ∈ s)], when unifying your theorem statement Lean will complain that the classical decidability is not the same as the concrete decidability instance (even though they're propositionally equal). This is always annoying when it happens, so it's best to just put the decidability in the theorem statement to prevent this kind of problem before it happens.