RFC: simp should not reduce tactic-defined lets.

[ericrbg]

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.

[leodemoura]

Did not read this RFC in detail, but it seems related to other issues, and be fixed by #2734

With the PR above, we have

/-
The first two example simplify because `simp` is using `decide` which will perform `zeta`.
-/
example : let l := 2; l = 2 := by
  simp (config := {zeta := false}) 

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

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

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

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

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

[ericrbg]

Hi Leo, sorry for being unclear and not actually leaving an mwe! Those examples were just for context, as I wasn't sure what the expected behaviour should be there.

I think the main issue we'd like to change is this:

example (a : Nat) : a + 1 - 1 = 37 := by
  let x := a + 1 - 1
  show x = _
  simp only
  -- I would like the goal to still be `x = _` without changing the default option.
  -- Goal is instead a + 1 - 1 = 37.
  sorry

I understand this can be done by setting simp's config to have zeta := false, but this is currently quite verbose to do and not very practical when many simps are involved, and so I was suggesting that this should be the default setting, or at least easy to access (say, for example, simpz being a tactic that has zeta := false by default and otherwise acts exactly like simp, or project-configurable simp defaults).

[ericrbg]

Leo, I'd just like to say that the main gist of this issue isn't fixed - I appreciate there's been many improvements, and the return of the simp [a] behaviour is very welcome! But a concise way to access simp with zeta disabled is I think very much still wanted in the mathlib community.

[kim-em]

Sorry about that, this might be due to error in my communicating with Leo. I'll reopen this now.

Would anyone, e.g. @ericrbg be willing to investigate what the breakage looks like if we were to change the default to zeta := false. I'm not sure this is a viable change to make, taking into account all users: we'd have to investigate. But it would be good to know what the fallout would be.

[ericrbg]

I've tried to make a start at this in my own fork (#2779), although I'm not really sure of many details of how to develop with this. One thing that this made me realise is the point that Kyle was talking about: I'd (personally) want that a goal of the form let n := 23 in n = 23 be reduced, but if you're in a tactic state and you have n : Nat := 23 and the goal is n = 23, I would not want this. If I understand this, Kyle said these are different.

I'm also struggling to find some tests; I can fix (or show there's issues) in the .lean files, but I cannot seem to find the .sh ones, such as leanlaketest_deps for one example.

[leodemoura]

@ericrbg @kmill @semorrison

Here is my current understanding.

1. Community wants us to split the zeta flag into two new flags:

• zeta1 : Given ... x : ty := val ... |- C[x], simp reduces it to ... x : ty := val ... |- C[val]
• zeta2 : Given .... |- C[let x : ty := val; e[x]], simp reduces it to ... |- C[e[val]]
  Please send suggestions to name the new flags.

2. Community wants zeta1 := false and zeta2 := true as the default setting for simp

Agreed?

[ericrbg]

Yes, I would agree with this! I'll post it in the Zulip thread too :)

[kim-em]

As naming suggestions, how about:

• zeta2 is just zeta (i.e. so sometimes people will use zeta := false to completely turn off zeta reduction)
• zeta1 is zeta_ctx (i.e. so sometimes people will use zeta_ctx := true to additionally do zeta reduction in the context)

[leodemoura]

As naming suggestions, how about:

• zeta2 is just zeta (i.e. so sometimes people will use zeta := false to completely turn off zeta reduction)
• zeta1 is zeta_ctx (i.e. so sometimes people will use zeta_ctx := true to additionally do zeta reduction in the context)

Great. Let's go with it.

[leodemoura]

@semorrison BTW, I will use zetaCtx to ensure the naming convention in consistent.