Zulip Chat Archive

Stream: new members

Topic: is simp "stable"?


view this post on Zulip Filippo A. E. Nuccio (Oct 17 2020 at 11:28):

I am wondering if simp is a "stable" tactic in the following sense. If I can finish a proof by

simp, exact h
end

where h is some local hypothesis that I have in my context, this is because after the application of simp the goal is exactly h. But if people keep adding new lemmas with the attribute @[simp], Lean might eventually become smarter and transform the goal (as it is before my application of exact h) to something nicer. Then I wonder if the tactic exact h will still work to conclude the proof.

view this post on Zulip Kenny Lau (Oct 17 2020 at 11:29):

that's why we discourage non-terminal usages of simp

view this post on Zulip Kenny Lau (Oct 17 2020 at 11:30):

(and I discourage simp in general but that's another topic)

view this post on Zulip Filippo A. E. Nuccio (Oct 17 2020 at 11:30):

Kenny Lau said:

that's why we discourage non-terminal usages of simp

Ah, and you meant to start your answer by "No, it won't work...", right? :hurt:

view this post on Zulip Ruben Van de Velde (Oct 17 2020 at 11:33):

Well, it might keep working... But you probably don't want to make that assumption

view this post on Zulip Filippo A. E. Nuccio (Oct 17 2020 at 11:34):

Ah gosh. But then simp is really a terrible tactic... or am I too conspirationist?

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 11:35):

Maybe simp [h] works? This would be fine.

view this post on Zulip Kenny Lau (Oct 17 2020 at 11:35):

Filippo A. E. Nuccio said:

Ah gosh. But then simp is really a terrible tactic...

tactics are tools with intended usages

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 11:37):

There are all sorts of tricks to make non-terminal simps terminal. For example, if h : P and if simp changes your goal into P today, then as we all know it might turn the goal into some different simpler P' tomorrow because of some clever PR, but if you write

suffices : P,
  simpa,
exact h

then this proof will not break even if simp learns how to simplify P later on.

view this post on Zulip Filippo A. E. Nuccio (Oct 17 2020 at 11:37):

Kevin Buzzard said:

Maybe simp [h] works? This would be fine.

First, let me clarify that mine is a hypothetical question (I have no issue at the moment with my code). That being said, I am not sure to follow: if I write simp [h] I am temporarily adding to all @[simp]'s lemma also h, so Lean is even smarter, no?

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 11:38):

If h is an equality then yes, you're temporarily making simp smarter, but the point is that you are now making it smart enough to close the goal. The rule is that simp should always close goals.

view this post on Zulip Filippo A. E. Nuccio (Oct 17 2020 at 11:40):

Ah, ok, I see. I wasn't aware of this rule. Thanks.

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 11:47):

It's a mathlib rule, not a general rule, but basically it's not ideal if you come back to your code in 1 years' time (like I just did with my undergraduate teaching material) and then find that parts of it don't compile with current mathlib (which fortunately did not happen to me this year).

view this post on Zulip Reid Barton (Oct 17 2020 at 12:15):

simpa using h exists for this purpose--it's approximately simp at h, simp, exact h and the idea is that if simp got smarter and kept simplifying the goal past the form of h, then hopefully it will simplify h in the same way.

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:14):

from a tooling point of view, it would be possible to just replace simp with a simp only automatically, so that it is stable. select a "simp" in your editor, hit some particular key combination, and it expands out. i'm not sure how much people would appreciate this; it might make a proof look uglier.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:25):

that would be squeeze_simp

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:26):

right, you could have your editor do that for you. i mean why do people use simp at all instead of squeeze_simping everything

view this post on Zulip Yakov Pechersky (Oct 19 2020 at 17:48):

The editor (VSCode) responds to the squeeze_simp trace output, with a Try this: ..., which is clickable, and replaces the squeeze_simp with a simp only [...], or whatever variant you used.

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:49):

i guess that is close to as easy as possible

view this post on Zulip Yakov Pechersky (Oct 19 2020 at 17:49):

I use just simp often in development when I am adding/removing simp lemmas, because such changes would quickly break any simp only

view this post on Zulip Yakov Pechersky (Oct 19 2020 at 17:50):

When I am in small branches of mathlib or something similar, such that the accessible simp set is small.

view this post on Zulip Yakov Pechersky (Oct 19 2020 at 17:51):

squeeze_simp is slow, because it tries to be minimal

view this post on Zulip Yakov Pechersky (Oct 19 2020 at 17:51):

as opposed to simp, which can make extra unnecessary changes as long as the final term is simplified

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:57):

plus squeeze_simp is noisy, so I usually wouldn't want more than one in the text at once

view this post on Zulip Mario Carneiro (Oct 19 2020 at 17:58):

usually I just use simp while developing and find/replace with squeeze_simp -> simp only during cleanup

view this post on Zulip Bryan Gin-ge Chen (Oct 19 2020 at 18:01):

I think we talked a bit before about renaming squeeze_simp to simp?, just to make it a bit easier to call. I forget what the obstacles there were though.

view this post on Zulip Golol (Oct 20 2020 at 15:15):

What about storing the proof term seperately somewhere in the library as a backup proof. That should be stable.

view this post on Zulip Yakov Pechersky (Oct 20 2020 at 15:18):

That's pretty similar to Kevin's "suffices" style above

view this post on Zulip Joe Hendrix (Jan 19 2021 at 07:52):

(deleted)


Last updated: May 15 2021 at 02:11 UTC