simp fails but rw succeeds

Stream: new members

[Rudy Peterson]

Hello,

Sometimes, simp [thm] fails, but rw [thm] succeeds. Other times, when I add a thm to the simp set via @[simp] it fails to rewrite with it with just simp. Sometimes I need to use simp_rw [thm] when neither simp [thm] nor rw [thm] works. Sometimes simp [thm] fails but simp [thm (param:=arg) succeeds.

I understand that this is a broad question, but why is this?

I am especially confused with simp fails to use something in the simp set via @[simp], and when rw [thm] succeeds but simp [thm] fails...

Thanks!

[Etienne Marion]

If your theorem requires hypotheses, then rw will apply it and generate goals for the side conditions, but simp and simp_rw won't do that.

[Rudy Peterson]

What if the theorem is of the form:

theorem thm {param_1} ... {param_n} : P <-> Q := by
  ...

[Aaron Liu]

simp will not rewrite arguments that are dependent, but rw will do it

[Aaron Liu]

since simp does the rewriting piecewise one at a time and every intermediate step has to typecheck, but rw substitutes all at once and then checks type correctness after, so sometimes rw can be more powerful than simp

[Rudy Peterson]

Sometimes, when I invoke simp [thm], it will rewrite with thm in one instance, but not for others, and then I need to manually also do simp [thm (param:=arg)]

[Rudy Peterson]

Aaron Liu said:

simp will not rewrite arguments that are dependent, but rw will do it

Interesting, thanks that's good to know! I don't think I have run into this issue yet...

Ah I have, but that's not the only place I guess...