typeclass inference failing with decidable pred

Stream: lean4

[Kevin Buzzard]

I am surprised that the second example below fails. Is there a way to make it work without explicitly supplying the instance?

def Nat.find (p : Nat → Prop) [DecidablePred p] (H : ∃ (n : Nat), p n) : Nat := 37

noncomputable instance Classical.DecidablePred (r : α → Prop) : DecidablePred r :=
λ _ => Classical.propDecidable _

noncomputable example (hr : ∃ N : Nat, N = N) : Nat :=
Nat.find _ hr -- works

noncomputable example (hr : ∃ N : Nat, ∀ n, N ≤ n) : Nat :=
Nat.find _ hr -- fails

noncomputable example (hr : ∃ N : Nat, ∀ n, N ≤ n) : Nat :=
@Nat.find _ (Classical.DecidablePred _) hr -- works

[Mario Carneiro]

Because DecidablePred is an abbreviation, lean isn't looking for or considering your Classical.DecidablePred instance. Instead, you need to make Classical.propDecidable available as an instance, and since it is a scoped instance open Classical suffices (although unfortunately open Classical.propDecidable or open Classical (propDecidable) don't work).

[Kevin Buzzard]

In which case I'm surprised the N=N example works!

[Kevin Buzzard]

Yes I understand my error now, DecidablePred isn't a class so this should never be working. Thanks!

[Mario Carneiro]

N = N is decidable because nat has decidable eq