Why does apply_instance fail to generate decidable_pred here?

Question

Here is a stripped down version of something that is causing me trouble.

variables {α : Type*} [decidable_eq α]

def S (a : α) : set α := λ b, b = a

def P (a : α) : decidable_pred (λ (c : α), c = a) := 
 by { apply_instance, }

def Q (a : α) : decidable_pred (λ (c : α), c ∈ (S a)) := 
 by { simp[S], apply_instance, }

Lean is happy with the definition of P, but rejects the definition of Q as follows:

tactic.mk_instance failed to generate instance for
  decidable_pred (λ (c : α), c ∈ λ (b : α), b = a)
state:
α : Type u_1,
_inst_1 : decidable_eq α,
a : α

In both P and Q, we ask tactic.mk_instance to generate a decision procedure for a predicate. The predicate in Q is equivalent under β-reduction to the one in P, but tactic.mk_instance succeeds with P but fails with Q. Is this just a weakness in the tactic or is there some more subtle issue? Is there some straightforward way to work around this kind of problem?

Answer 1

The predicate in Q is equivalent under β-reduction to the one in P

Not according to Lean in this case. set.mem is a def, which are not unfolded during typeclass inference by default. Thus inference fails at unifying it with =:

set_option trace.type_context.is_def_eq_detail true

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 a_1 : decidable ((λ (c : α), c ∈ λ (b : α), b = a) a_1) := _inst_1 (?x_1 a_1) (?x_2 a_1)
[type_context.is_def_eq_detail] [1]: decidable ((λ (c : α), c ∈ λ (b : α), b = a) a_1) =?= decidable (?x_1 a_1 = ?x_2 a_1)
[type_context.is_def_eq_detail] [2]: (λ (c : α), c ∈ λ (b : α), b = a) a_1 =?= ?x_1 a_1 = ?x_2 a_1
[type_context.is_def_eq_detail] after whnf_core: a ∈ λ (b : α), b = a_1 =?= ?x_1 a = ?x_2 a
[type_context.is_def_eq_detail] [3]: @set.mem α a (λ (b : α), b = a_1) =?= ?x_1 a = ?x_2 a
[type_context.is_def_eq_detail] [4]: set.mem =?= eq
[type_context.is_def_eq_detail] on failure: set.mem =?= eq
[type_context.is_def_eq_detail] on failure: @set.mem α a (λ (b : α), b = a_1) =?= ?x_1 a = ?x_2 a
[type_context.is_def_eq_detail] on failure: decidable ((λ (c : α), c ∈ λ (b : α), b = a) a_1) =?= decidable (?x_1 a_1 = ?x_2 a_1)
failed is_def_eq

We can fix this with either local attribute [reducible] set.mem or simp[S, set.mem].

This still begs the question, why is set.mem (and others, including set itself) not marked as reducible? AFAIR this was a conscious decision to prevent it from "unexpectedly" unfolding and thus mixing the "world of sets" with the "world of predicates". People usually think of them as separate concepts, so it can be confusing when your goals are suddenly switched to the other world.

Answer 2

I'm not sure about the exact meaning of the question. But indeed apply_instance is simply not trying to do β-reduction before working.

variables {α : Type*} [decidable_eq α]

def S (a : α) : set α := λ b, b = a

def P (a : α) : decidable_pred (λ (c : α), c = a) := 
 by { apply_instance, }

def Q (a : α) : decidable_pred (λ (c : α), c ∈ (S a)) := 
show decidable_pred (λ (c : α), c = a),  by apply_instance

certainly works.