Zulip Chat Archive

Stream: general

Topic: Let binding efficiency


view this post on Zulip Seul Baek (Dec 24 2018 at 00:04):

If a term foo appears multiple times in a definition in such a way that each occurrence of it will have to be normalized, does the definition become more efficiently computable by using let x := foo in in the beginning? The assumption is that x will be structured in a way that forces (some) normalization with the let binding (e.g., if foo : A × B, then let (a,b) := foo).

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:08):

yes, although lean does that sometimes on its own, during the common subexpression elimination pass

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:08):

do you mean in the VM or the kernel?

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:09):

Note that let (a,b) := foo is not a let binding at all, it is just notation for a recursor

view this post on Zulip Seul Baek (Dec 24 2018 at 00:10):

I meant the kernel, although I'd be curious about the VM as well.

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:11):

In the kernel, I am not positive but I would guess that it depends on how shared the expression object is in memory

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:11):

using a let binding like that is a good way to make sure that the same expression object is used in each place

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:12):

but there will be some overhead with unfolding it

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:12):

The kernel caches the whnf operation, so it won't need to calculate it many times if it is asked for multiple times

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:13):

but I'm not sure whether the same expression in different contexts can cause a problem (since this might mean renaming vars and unsharing)

view this post on Zulip Seul Baek (Dec 24 2018 at 00:17):

The main downside I'm experiencing with let is that it doesn't play nice with the simplifier when I have to prove properties about definitions which include it (_match_1 all over the place) and requires extra definitional lemmas for unfolding. So I was wondering if there are reasons to use it other than its concision.

view this post on Zulip Seul Baek (Dec 24 2018 at 00:20):

If let (a,b) := foo is not a let binding, is there something else I can do to normalize foo and bind it to fresh term(s)?

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:33):

like I said, it's just a recursor. If you don't like the _match_1 stuff, you can use tactics instead to construct the term, which don't leave this junk in the term

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:33):

i.e. by cases foo with a b; exact

view this post on Zulip Mario Carneiro (Dec 24 2018 at 00:33):

it's equivalent to writing prod.rec explicitly in the term

view this post on Zulip Seul Baek (Dec 24 2018 at 00:51):

I see. Thanks!


Last updated: May 14 2021 at 00:42 UTC