dsimp and simp

Stream: mathlib4

[Jireh Loreaux]

I think this is different, but I could be wrong. I think the point is that it is h that is being dsimped before the simp call.

[Floris van Doorn]

Yaël Dillies said:

That also means simp isn't strictly more powerful than dsimp anymore, right? We really should make a warning about that, then.

simp has not been strictly more powerful than dsimp since forever, unless you mean something different by "strictly more powerful" than I do. dsimp is able to simplify arguments of dependent functions.

[Mario Carneiro]

actually I think simp is strictly more powerful in that sense in lean 4, simp will go into "dsimp mode" if it can't traverse into a dependent function argument

[Mario Carneiro]

but no this does not mean that simp no longer subsumes dsimp, because dsimp got less powerful in exactly the same way

[Mario Carneiro]

if you do dsimp [h] well it won't do anything at all because h is a local variable, but if h was a theorem with that type that was proved by rfl then dsimp [h] would have worked and no longer does, and dsimp only at h; dsimp [h] would in theory work but it doesn't make sense to dsimp a global theorem so you would just have to restate the theorem without the bad LHS