Zulip Chat Archive

Stream: general

Topic: What should be @[simp]?


view this post on Zulip Yufan Lou (Feb 24 2020 at 04:34):

I put @[simp] on my leftpad definition to demonstrate it, but it definitely cannot be applied to everything. Are there any rules to which I can refer?

view this post on Zulip Johan Commelin (Feb 24 2020 at 04:46):

Rules of thumb: @[simp] should be applied to

  • only lemma or theorem, not to def
  • only things of the form foo = bar or xyzzy = quux
  • only if the LHS is "more complex" and the RHS is "simpler"

view this post on Zulip Johan Commelin (Feb 24 2020 at 04:47):

There are exceptions to these rules, and also the rules are maybe not complete. But they give the rough idea.

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:00):

now to go back and rewrite my proof :upside_down:

view this post on Zulip Floris van Doorn (Feb 24 2020 at 18:52):

You can also add @[simp] to definitions. This will tell simp that it can unfold this definition.

view this post on Zulip Scott Morrison (Feb 24 2020 at 20:13):

:up: Use with caution!

If you're defining a structure, you should use @[simps] in preference to @[simp], as this defines simp lemmas for each of the structure projections, but doesn't allow unfolding the entire definition.


Last updated: May 14 2021 at 12:18 UTC