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 simp
s? 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