simp vs explicitly using lemmas

Stream: new members

[Angela Li]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Angela Li]

Okay, thank you!