Zulip Chat Archive

Stream: general

Topic: simpa using h vs simp at h, simp [h]


view this post on Zulip Sean Leather (Sep 17 2018 at 07:01):

On a few occasions, I've found that simp at h, simp [h] works when simpa using h does not. I thought the latter was intended to replace the former. Is this not the case?

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:08):

They are not equivalent. simpa using h is equivalent to simp at h |-, exact h

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:09):

in particular, simp at h, simp [h] may use h to rewrite in subterms, while simpa is just preparing to match it directly against the goal

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:11):

This makes simpa less powerful but more controlled, especially when quantifiers get involved

view this post on Zulip Sean Leather (Sep 17 2018 at 07:11):

Ah, okay. Thanks.

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 07:56):

Sean -- do you fancy editing the simp docs to explain this? I never really feel on top of this subtlety so never feel equipped to change them to explain it. I am still at the stage where I just try random combinations of simp, simpa, simp!, simp * at * and just keep going until it works.

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 07:57):

https://github.com/leanprover/mathlib/blob/master/docs/extras/simp.md

view this post on Zulip Kevin Buzzard (Sep 17 2018 at 07:58):

Just edit the community one I guess

view this post on Zulip Sean Leather (Sep 17 2018 at 08:13):

Hmm, I don't know. I'm just looking at that document for the first time. I don't find it very easy to follow for reference, and I wouldn't know where to put what. I think Mario answering Zulip questions in a document would be better. :wink:

view this post on Zulip Sean Leather (Sep 17 2018 at 13:50):

To make matters even more interesting, I have a goal that isn't solved by by simp at h, simp [h] but is solved by by simp at h; simp; exact h or by simp at h; simp [h] {contextual := tt} or λ x, by simpa using h x. After by simp at h; simp, h and the goal look exactly the same (with set_option pp.all true). I'm not clear on why it can't be solved.


Last updated: May 15 2021 at 22:14 UTC