Zulip Chat Archive

Stream: general

Topic: Singleton to property


Alice Laroche (Aug 16 2021 at 22:20):

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 (Aug 16 2021 at 22:28):

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 (Aug 16 2021 at 22:31):

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

Kyle Miller (Aug 16 2021 at 22:32):

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

Alice Laroche (Aug 16 2021 at 22:40):

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

Kyle Miller (Aug 16 2021 at 22:43):

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

Last updated: Dec 20 2023 at 11:08 UTC