non-terminal simps

Stream: lean4

[Connor Gordon]

When learning Lean 3, I was told that it's considered bad practice to have an unconstrained simp that's not at the end of a proof, and instead should use simp only [blah]. To help with this, if I recall correctly there was a squeeze_simp tactic in Lean 3 that helped to convert a simp to a simp only by listing what results simp was using, but in Lean 4 it doesn't seem to exist (or at least not under the same name)

Is this still a convention in Lean 4 to not have non-terminal simps? If so, is there a good way to figure out exactly what simp is doing?

[Adam Topaz]

Lean4 has simp?

[Adam Topaz]

A huge bonus in lean4 is that dsimp? actually does something useful now!

[Matthew Ballard]

In exchange for ext? :)

[Adam Topaz]

:(

[Adam Topaz]

ext needs some love. I realized today that ext A B doesn't work (sometimes? maybe all the time?) and often an additional intro B is needed.

[Adam Topaz]

But that''s something to be discussed elsewhere. For this thread, the OP should be perfectly happy with simp? :)

[Matthew Ballard]

Yes, that works great!

[Matthew Ballard]

In Lean 3 too also (unless I am hallucinating)

[Kevin Buzzard]

simp? worked in Lean 3 but was less reliable than squeeze_simp. On the other hand squeeze_dsimp existed in Lean 3 and always gave the answer dsimp only whatever the actual answer was ;-)

[Jon Eugster]

Matthew Ballard said:

In exchange for ext? :)

A while ago I implemented ext? in std4#120, it's just waiting for CI approval and review ;)

[Jireh Loreaux]

@Jon Eugster can you take advantage of the new code actions features that Mario implemented? That is, can you make the "Try this:" clickable and substitutable as it was in Lean 3?

[Jakob von Raumer]

Is there a way to properly use simp? in a situation like generates_multiple_goals <;> simp? where the output shown only provides the output for the first simp? invocation?

[Mario Carneiro]

wrap it in squeeze_scope (from Std.Tactic.SqueezeScope)