Attitude toward simp

Stream: new members

[Matt Diamond]

In a recent thread there was a question about proving the equality of max and max'. I suggested by rw [finset.max', with_bot.coe_unbot] and this worked, but only after the user updated their mathlib to master. It turns out that max' was changed to use unbot only a few days ago; previously it used option.get, so the solution would have worked with option.coe_get instead of with_bot.coe_unbot.

It occurred to me that with_bot.coe_unbot and option.coe_get are both simp lemmas, meaning that if I had initially suggested by simp [finset.max'] it would (in theory) have worked without the user needing to update mathlib. Of course, maybe it's a good thing that they updated mathlib, but my point here is that using simp appears to make code more robust against changes to mathlib, as it chooses the appropriate lemma dynamically instead of relying on a specific one. This benefit of using simp hadn't occurred to me before.

Should I have suggested by simp [finset.max'] instead of by rw [finset.max', with_bot.coe_unbot]? More generally, does this robustness mean we should prefer using simp (in our own code and in suggestions to others) even when it only performs one additional rewrite?

[Violeta Hernández]

My opinion on simp is that if you need to specify any additional lemmas, you're most likely using it wrong

[Violeta Hernández]

It's not really based on much other than anecdote

[Violeta Hernández]

I guess I can try to elaborate: if you have to use additional lemmas on a simp, one of two things is likely happening

• the lemma should be marked simp but isn't, that's an easy fix
• you're doing some rewrites then finishing a proof by simp, in which case I believe it's cleaner to separate the steps out

[Violeta Hernández]

Of course, that additional lemma might be a local hypothesis, or there might be the rare case where that hypothesis appears multiple times in the expression and allows for further simplification: using simp with extra hypotheses is fine in that case

[Violeta Hernández]

My opinion on using simp for didactic purposes: don't

[Violeta Hernández]

It's a very useful tactic but it's hard to understand if you don't already have a clear understanding of what the lemmas it can use are

[Damiano Testa]

I was the "user" that Matt refers to! :smile:

My attitude towards simp is somewhat the opposite of what Violeta said: once I realize that a proof can end with simp, I then try to absorb as many lines before it as possible into the simp.

I find that this makes code much less brittle, precisely for the reason that Matt mentions: simp will try snake its way around lemmas, and if it needs some hints, then I'll make its life easier!

Ultimately, it is probably a question of whether you want to do small fixes every time you change a lemma that is used in a rw, or whether you prefer to do them only when a simp [stuff] no longer works. The second issue feels its like much less frequent, though it could be harder to fix than the former.

[Yaël Dillies]

Adding lemmas to a simp is actually a very sane thing to do. This usually happens when the simplification of an expression, except for one or two steps that "complicate" it.

[Moritz Doll]

One could also argue that this makes the proofs more readable since it basically says 'simplify and use these nontrivial facts' and it is way easier to understand than simp only [..], rw complicated_lemma, simp.

[Bjørn Kjos-Hanssen]

What do y'all think of this: "You should understand your Lean code so well that tactics are something you want to use, but not something you need to use"

[Adam Topaz]

I'm not so sure about that statement, particularly the word "understand". In my experience, after a while you just build up intuition for what tactics will make progress. And concerning simp, I personally found that I used simp more and more with more experience. After a while you realize just how powerful simp can be, and you want to use it as much as possible.

[Jim Fowler]

I am a little worried about excessive simp and using "backwards" simp and I wonder if there might be something clearer to write. For example, with squeeze_simp I was able to produce https://github.com/leanprover-community/mathlib/blob/psl/src/linear_algebra/special_linear_group.lean#L246-L262 which includes code like

  simp only [coe_scalar, special_linear_group.coe_fn_eq_coe, special_linear_group.coe_inv] at ⊢ ha,
  simp only [← ha, ← diagonal_one, ← diagonal_smul, adjugate_diagonal],
  simp only [diagonal_smul, diagonal_one, pi.smul_apply, algebra.id.smul_eq_mul, mul_one,
    finset.prod_const, finset.card_erase_of_mem, finset.mem_univ],
  simp only [← diagonal_one, ← diagonal_smul, matrix.diagonal_eq_diagonal_iff],
  simp only [pi.smul_apply, algebra.id.smul_eq_mul, mul_one, eq_self_iff_true, implies_true_iff],

It seems that I can't collapse these because of the use of ←?

[Rob Lewis]

@Jim Fowler Often, when you end up with a huge pile of simps like this, it's a sign that you've unfolded too much. A few lemmas there stand out as being too "low level" for what you're trying to do: pi.smul_apply, all the finset stuff, ...

Here's a more direct proof. I started the same way you did, squeeze_simp at ha ⊢, then noticed I could rewrite with ha and the proof fell out from there.

  simp only [coe_scalar, special_linear_group.coe_fn_eq_coe, special_linear_group.coe_inv] at ⊢ ha,
  rw [← ha, adjugate_smul, adjugate_one],
  refl

[Jim Fowler]

That's so great!