Zulip Chat Archive

Stream: general

Topic: simp_proj


view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 08 2019 at 23:36):

Can we automate these with an attribute @[simp_proj], which automatically generates these?

view this post on Zulip Scott Morrison (May 08 2019 at 23:36):

mathlib is accumulating hundreds of lemmas that could all be automated away in this way.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (May 09 2019 at 23:46):

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/automatic.20simp.20lemmas/near/151823722


Last updated: May 08 2021 at 03:17 UTC