Zulip Chat Archive

Stream: lean4

Topic: non-terminal simps


Connor Gordon (May 17 2023 at 22:58):

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 (May 17 2023 at 22:59):

Lean4 has simp?

Adam Topaz (May 17 2023 at 22:59):

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

Matthew Ballard (May 17 2023 at 23:00):

In exchange for ext? :)

Adam Topaz (May 17 2023 at 23:00):

:(

Adam Topaz (May 17 2023 at 23:01):

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 (May 17 2023 at 23:02):

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

Matthew Ballard (May 17 2023 at 23:02):

Yes, that works great!

Matthew Ballard (May 17 2023 at 23:02):

In Lean 3 too also (unless I am hallucinating)

Kevin Buzzard (May 17 2023 at 23:10):

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 (May 19 2023 at 06:38):

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 (May 19 2023 at 11:28):

@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?


Last updated: Dec 20 2023 at 11:08 UTC