let vs letI for local instances

Stream: mathlib4

[Eric Wieser]

In lean 3, we almost always used letI for local instances, and mathport translated this literally.

Of course, the I inletI now means something totally different to what it did in Lean 3 (now "inline" instead of "instance"), so this translation, while harmless, might not be a practice we want to continue to proliferate.

The main advantages of letI over let here are:

• It's already in our muscle memory
• It generates a name for the instance for us

while the disadvantage is:

• It perpetuates the incorrect mnemonic for the I
• The fact it inlines is seemingly irrelevant most of the time

[Oliver Nash]

I'd also be interested to know why let and letI must both exist (and likewise have and haveI). Mathematically there's no difference.

[Eric Wieser]

letI is handy in term mode for when you want to build a statement piece-by-piece, but want the result to look like it was built all at once

[Eric Wieser]

We actually did use this in a handful of places in mathlib3; by have := x; exact y was analogous to lean 4's haveI := x; y

[Oliver Nash]

Eric Wieser said:

letI is handy in term mode for when you want to build a statement piece-by-piece, but want the result to look like it was built all at once

I believe I understand why letI is superior to let in this case. Is there an example where let is superior to letI?

[Eric Wieser]

Yes, you can tell simp not to unfold lets (though annoyingly Lean4 changed the default to be that they are unfolded)

[Eric Wieser]

I also remember a case recently where letIs caused a timeout but let did not.

[Oliver Nash]

Thanks, I guess I'd need to see some examples to decide if this means to control simp unfolding is a useful feature.

[Oliver Nash]

I'm mentally filing this as "let vs letI is seldom important and probably something that should not exist but has to for now".

[Eric Wieser]

I think there's also an organizational reason here; letI is not in core but std, IIRC

[Eric Rodriguez]

Oliver Nash said:

Thanks, I guess I'd need to see some examples to decide if this means to control simp unfolding is a useful feature.

try read the mathported Wedderburn's little theorem proof right now... because of simp unfolding let bindings it's not easy to read the goal

[Eric Rodriguez]

on the other hand letI makes cleaner terms; docs#Nat.recOnPrimePow I changed to only use letI + haveI so that the term is only like Nat.strongRecOn ... (fun ... ih => Eq.mpr _ ih) as opposed to a bunch of let bindings hidden in there