Zeta-reducing have expressions

Stream: lean4

[Aymeric Fromherz]

Hi, as part of a tactic, I'm trying to normalize let-bindings by calling Lean.Meta.zetaReduce. However, this function does not seem to work with have expressions. In the following code, when the letToHave rewriting is enabled, applying tactic foodoes not modify the goal.
This seems surprising since have expressions appear to be reduced using zeta in simp. Is there an option to enable this, or a different helper to call to reduce both lets and haves? Thanks!

import Lean
open Lean Elab Term Meta Tactic

elab "foo" : tactic => withMainContext do
  let goal ← getMainTarget
  let reducedGoal ← zetaReduce goal
  Lean.logInfo m!"before reduction {goal}"
  Lean.logInfo m!"after reduction {reducedGoal}"

-- set_option cleanup.letToHave false

def f (n: Nat): Nat :=
  let m := n+1
  m-1

example: f 0 = 0 := by
  unfold f
  foo
  sorry

[Chris Bailey]

The meta expressions for reduction generally do not traverse into subterms, while simp does. You can do something like this.

I had to use whnfCore, I'm actually not sure why zetaReduce does not seem to succeed in that context.

[Robin Arnez]

You can modify the existing function slightly to make your use case work:

def zetaHaveReduce (e : Expr) : MetaM Expr := do
  let pre (e : Expr) : MetaM TransformStep := do
    let .fvar fvarId := e | return .continue
    let some localDecl := (← getLCtx).find? fvarId | return .done e
    let some value := localDecl.value? (allowNondep := true) | return .done e
    return .visit (← instantiateMVars value)
  transform e (pre := pre) (usedLetOnly := true)

(note the additional allowNondep in comparison to the original source)

[Robin Arnez]

There's probably some argument to be made though that this should be the default behavior.

[Aymeric Fromherz]

Thanks! This does fix my issue. I opened an issue on Github with your suggested fix, in case this should indeed be the default behavior