## Stream: new members

### Topic: is simp "stable"?

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

#### Kenny Lau (Oct 17 2020 at 11:29):

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

#### Kenny Lau (Oct 17 2020 at 11:30):

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

#### 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:

#### 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

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

#### Kevin Buzzard (Oct 17 2020 at 11:35):

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

#### 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

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

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

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

#### Filippo A. E. Nuccio (Oct 17 2020 at 11:40):

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

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

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

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

#### Mario Carneiro (Oct 19 2020 at 17:25):

that would be squeeze_simp

#### 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

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

#### Kevin Lacker (Oct 19 2020 at 17:49):

i guess that is close to as easy as possible

#### 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

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

#### Yakov Pechersky (Oct 19 2020 at 17:51):

squeeze_simp is slow, because it tries to be minimal

#### 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

#### 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

#### 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

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

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

#### Yakov Pechersky (Oct 20 2020 at 15:18):

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

#### Joe Hendrix (Jan 19 2021 at 07:52):

(deleted)

Last updated: May 15 2021 at 02:11 UTC