simp and local lets

Stream: lean4

[Bhavik Mehta]

How is simp meant to interact with local lets now? I know there were some changes fairly recently but the behaviour doesn't seem to make sense to me right now:

I have two lets c and d in my local context, and simp only is unfolding d and not c, which is confusing behaviour to me. In particular this is annoying because I'd like to do the exact opposite (unfold c and not d), and I was hoping that simp only [c] would work, but it's going way too far.

Here's an example with no dependency on mathlib

variable {α : Type}

theorem test {n : Nat} {f : Fin n → α} : False := by
  let c (i : Fin n) : Nat := i
  let d : Fin n → Nat × Nat := fun i => (c i, c i + 1)
  have : ∀ i, (d i).2 ≠ c i * 2 := by
    simp only

The simp only unfolds d but not c. What I actually wanted - in the original context - was to unfold c but not d, which I'd do with simp only [c]. But since simp only is unfolding d too, this breaks my proof idea. How can I use simp or variants on a goal like this?

[Bhavik Mehta]

The same thing happens when turning the config option zeta off too. zetaDelta says it's off by default, although this example seems to be exactly a zetaDelta reduction, but turning it off explicitly doesn't help either.

[Ruben Van de Velde]

I'm surprised as well that d would be unfolded

[Bhavik Mehta]

To make it even more surprising, changing d to fun i => c i returns the behaviour back to normal!

[Damiano Testa]

Mathlib has unfold_let c: does that do what you want? It still does not answer why simp starts unfolding the latest let, but maybe it is good as a workaround.

[Bhavik Mehta]

Ah yeah this is a nice workaround in my context, thanks. (The workaround I was using was to generalize to force simp only not to unfold too far, but yours is cleaner!) edit: unfortunately not, because I want to simp only with some other lemmas afterwards, and that one goes too far instead

[Floris van Doorn]

Turning the proj option off does what you want in this case:

theorem test {α : Type} {n : Nat} {f : Fin n → α} : False := by
  let c (i : Fin n) : Nat := i
  let d : Nat × Nat := (1, 2)
  have : ∀ i, d.2 ≠ c i * 2 := by
    simp (config := {proj := false}) only [c]

I think it's a good idea to have the "projection-reduction" be aware of the zetaDelta (and zeta) options, and be more conservative if they are off.

[Floris van Doorn]

maybe open an RFC?

[Floris van Doorn]

lean4#5455 (to keep things linked)

[Bhavik Mehta]

Oops sorry, meant to do this myself. Thanks!

[Tomas Skrivan]

Last time I investigated a similar issue the offending call to whnf is in project? which is called in reduceProj? which is called in reduceProjFn? which is part of the simplifier. I think that whnf call should inherit config from the simplifier. However I'm not sure what to do about whnf cache.

[Tomas Skrivan]

The similar issue is that

(let a:=x+x; let b:= x*x; (a,b)).1

reduces to

x+x

instead of to

let a:= x+x; a

with zeta:=false

I will reinvestigate this and comment on the GitHub issue.