Proposal

simp should not define tactic-defined lets (maybe these are called fvars) by default, or at least the option to do so should be one character, as opposed to having to use (config := {zeta := false}).

In mathlib, the main way lets are used are to abstract some details of the proof; for example the following pattern:

	let q := my_complicated_object a b 37 42
	have : P q := sorry
	have : Q q := sorry
	-- work with only the properties `P q` and `Q q`, not the definition of `q` itself.

is very common, because my_complicated_object a b 37 42 is a lot more mental strain to read than q; when this object appears many times in the goal, it can often be overwhelming.

However, this illusion of abstraction is currently broken every time we use simp, as the default option to unfold let bindings means that no matter our carefully packaged lets, we lose the details of such things every time, and the mental strain comes back, or we have to put a lot of changes to keep the goal under control.

There is already many ways to control let unfolding, with extra tools added in Mathlib. I think people were happy with the Lean3 status quo that if a let was to be unfolded, then we could just expressly put that into simp (i.e. by let a := b, simp [a]); this doesn't seem to work in Lean4 either, but this is not the key issue.

My proposed solution is simply that the default config option is zeta := false; this has an almost-zero maintainability burden bar the first refactoring for proofs that need it. There may be cleverer solutions that hopefully also don't require much more burden; see Kyle's comment below.

Community Feedback

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20unfolding.20let.20bindings is a thread discussing this issue. Within this limited sample, I see very little dissent, although this comment from Kyle is interesting:

Maybe the zeta configuration should be split into two, one that controls substitution of fvars (what the poll is about) and one that controls whether let expressions are reduced (which I presume the poll isn't about)

I'm personally unsure about the details of this, but there is clearly something delicate going on:

example : let l := 2; l = 2 := by
  simp (config := {zeta := false})

example : let l := 2; l = 1 := by
  simp (config := {zeta := false})

example (t : Nat) : let l := t; l = 2 := by
  simp (config := {zeta := false})

example (t : Nat) : let l := 2; t = l := by
  simp (config := {zeta := false})

In these examples, the first goal is closed, the second one is reduced to False, and the third and fourth are untouched. I'm not sure why.

There seems to have been an attempt to change this here: https://github.com/PatrickMassot/lean4/releases/tag/zeta_false2.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.