Singleton to property

Stream: general

[Alice Laroche]

I can't find a way to prove that :

example (T : Type) (p : set T) (x : T) (h : p = {x}) : p x :=
begin

end

[Kyle Miller]

This works:

example (T : Type) (p : set T) (x : T) (h : p = {x}) : p x :=
begin
  rw h,
  exact rfl,
end

However, this use of a set is "breaking the set API". Lemmas assume that you either use ∈ like in

example (T : Type) (p : set T) (x : T) (h : p = {x}) : x ∈ p :=
begin
  rw h,
  apply set.mem_singleton,
end

or use set_of or {y | p y} to turn a predicate into a set

example (T : Type) (p : T → Prop) (x : T) (h : set_of p = {x}) : p x :=
begin
  rw ←@set.mem_set_of_eq T x p,
  rw h,
  apply set.mem_singleton,
end

[Alice Laroche]

Yeah i know i shouldn't use set like this, but actually it's the simp tactic who do that...

[Kyle Miller]

Would you create a #mwe that shows the simp tactic doing this? It would be helpful to debug simp.

[Alice Laroche]

Hmmm, sorry, will trying to create a mwe i figured i made a mistake 5 layers aboves

[Kyle Miller]

I'm confused why set.mem_def can't be used to rewrite p x without giving p explicitly here:

example (T : Type) (p : set T) (x : T) (h : p = {x}) : p x :=
begin
  --rw ←set.mem_def, -- not ok
  -- rewrite tactic failed, did not find instance of the pattern in the target expression
  --  ?m_1 ?m_2
  rw ←@set.mem_def _ _ p, -- ok
  rw h,
  apply set.mem_singleton,
end