Zulip Chat Archive
Stream: general
Topic: simp_proj
Scott Morrison (May 08 2019 at 23:35):
If I define def f (n : nat) : F := { a := 0, b := n + 17 } (for some structure F with fields a and b) it's usually a bad idea to mark this with the attribute @[simp], because then dsimp will unfold f 13. On the other hand, it's usually a good idea to tediously write simp lemmas for the projections, e.g. @[simp] lemma f_b (n : nat) : (f n).b = n + 17.
Scott Morrison (May 08 2019 at 23:36):
Can we automate these with an attribute @[simp_proj], which automatically generates these?
Scott Morrison (May 08 2019 at 23:36):
mathlib is accumulating hundreds of lemmas that could all be automated away in this way.
Floris van Doorn (May 09 2019 at 05:36):
We had an attribute in Lean 2 ([constructor]) which did basically this. It was very useful.
Scott Morrison (May 09 2019 at 23:39):
Another alternative would be something that guessed the simp lemma from the name, and built it for you. Sometimes it's only certain chains of projections that you want simplified. E.g. currying_obj_obj_map
Reid Barton (May 09 2019 at 23:46):
Last updated: Dec 20 2023 at 11:08 UTC