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

Stream: general

[Sean Leather]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

Ah, okay. Thanks.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

Just edit the community one I guess

[Sean Leather]

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:

[Sean Leather]

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.