Simp on let bindings

Stream: lean4

[Tomas Skrivan]

There is a bit unintuitive behavior of simp
on let bindings when doing only a single pass.

I have a dummy identity function foo which I want to eliminate from an expression in a single pass of a simplifier. In case of let bindings this does not happen.

I would consider this as a bug but I'm not sure.

mwe

def foo {α} (a : α) := a

@[simp]
theorem foo_simp : foo a = a := by rfl

-- problematic case - two `foo` are still there
example :
  (let a := foo 0
   let b := foo a
   let c := foo b
   c) = 0 :=
by
  conv =>
    lhs
    simp (config := {singlePass := true}) only [foo_simp]
    trace_state -- foo (foo 0)

-- all `foo` are gone
example :
  (let a := foo 0
   let b := foo a
   let c := foo b
   c) = 0 :=
by
  conv =>
    lhs
    simp (config := {singlePass := true, zeta := false}) only [foo_simp]
    trace_state -- let a := 0; let b := a; let c := b; c

-- all `foo` are gone
example :
  foo (foo (foo 0)) = 0 :=
by
  conv =>
    lhs
    simp (config := {singlePass := true}) only [foo_simp]
    trace_state -- 0

To fix this I propose to change this line

      return { expr := b.instantiate1 v }

to

      simp (b.instantiate1 v)