is simp "stable"?

Stream: new members

[Filippo A. E. Nuccio]

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.

[Kenny Lau]

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

[Kenny Lau]

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

[Filippo A. E. Nuccio]

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:

[Ruben Van de Velde]

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

[Filippo A. E. Nuccio]

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

[Kevin Buzzard]

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

[Kenny Lau]

Filippo A. E. Nuccio said:

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

tactics are tools with intended usages

[Kevin Buzzard]

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.

[Filippo A. E. Nuccio]

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?

[Kevin Buzzard]

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.

[Filippo A. E. Nuccio]

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

[Kevin Buzzard]

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).

[Reid Barton]

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.

[Kevin Lacker]

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.

[Mario Carneiro]

that would be squeeze_simp

[Kevin Lacker]

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

[Yakov Pechersky]

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.

[Kevin Lacker]

i guess that is close to as easy as possible

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

squeeze_simp is slow, because it tries to be minimal

[Yakov Pechersky]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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.

[Golol]

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

[Yakov Pechersky]

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

[Joe Hendrix]

(deleted)