Zulip Chat Archive

Stream: new members

Topic: simp vs explicitly using lemmas


view this post on Zulip Angela Li (Jul 19 2020 at 14:27):

Hi. Would it be better to write @simp lemmas and use simp or to explicitly use exact and rw to finish proofs?

view this post on Zulip Scott Morrison (Jul 19 2020 at 14:38):

As long as they are good simp lemmas, then simp lemmas are great. Investing in writing good simp lemmas makes everything easier for people who use your definitions later.

view this post on Zulip Scott Morrison (Jul 19 2020 at 14:39):

Sometimes simp gets slow, but worry about that when you get there!

view this post on Zulip Scott Morrison (Jul 19 2020 at 14:39):

Do make sure simp lemmas really are "simplifying" according to some reasonable measure. And think a bit about what "simp normal form" you want to have, as you're selecting which lemmas to mark with @[simp].

view this post on Zulip Angela Li (Jul 19 2020 at 15:08):

Okay, thank you!


Last updated: May 14 2021 at 04:22 UTC