Zulip Chat Archive

Stream: general

Topic: simp does not use mem_singleton_iff


Rémy Degenne (Feb 16 2021 at 16:12):

The lemma set.mem_singleton_iff is marked as simp, but simp does not use it in the following example:

import data.set.basic

example {α} (s t : α) (ht : t  ({s} : set α)) : t = s :=
set.mem_singleton_iff.mp ht -- succeeds

example {α} (s t : α) (ht : t  ({s} : set α)) : t = s :=
by simp [ht] -- fails

How can I find out what happens here? I don't know how to get information about what simp tries. Am I wrong to expect simp to work here?

Eric Wieser (Feb 16 2021 at 16:12):

docs#set.mem_singleton_iff for reference

Rémy Degenne (Feb 16 2021 at 16:24):

example {α} (s t : α) (ht : t  ({s} : set α)) : t = s :=
by simpa using ht -- succeeds

But simpa works. I guess that the hypothesis ht can be simplified by simpa to match the goal. On the other hand the goal is already in its most simplified form and simp [ht] does not modify the hypothesis ht, which then never matches with the goal.

Yakov Pechersky (Feb 16 2021 at 16:29):

Correct. by simpa using ht simplifies both the goal and ht in a way to get them to align, and no further. So very similar to how this works:

example {α} (s t : α) (ht : t  ({s} : set α)) : t = s :=
by { simp at ht, exact ht }

Yakov Pechersky (Feb 16 2021 at 16:29):

Other possibilties are:

example {α} (s t : α) (ht : t  ({s} : set α)) : t = s :=
by rwa set.mem_singleton_iff at ht -- succeeds

example {α} (s t : α) (ht : t  ({s} : set α)) : t = s :=
by rwa set.mem_singleton_iff -- succeeds

Rémy Degenne (Feb 16 2021 at 16:42):

Ok, thanks for the help.


Last updated: Dec 20 2023 at 11:08 UTC