Simplifying only the first level of `let` bindings

Stream: lean4

[Malcolm Langfield]

Suppose I have the following:

  def f (n : Nat) : Nat :=
    let n₁ := n + 1
    let n₂ := n₁ + 1
    n₂

  example : f 2 = 4 := by
    unfold f
    simp (config := {zeta := False}) only

The goal looks like this after the unfold.

▶ 1 goal
s₀ s₁ : State
fuel : ℕ
⊢ (let n₁ := 2 + 1;
  let n₂ := n₁ + 1;
  n₂) =
  4

How can I zeta-reduce just the first let?

[Mario Carneiro]

I don't think there is any tactic that will do this, but you can write your own

[Malcolm Langfield]

Thanks for the answer, that sounds promising. Let me ask a different but related question: how can I write a tactic to do this?

I have a beginner's familiarity with tactic writing and stuff in MetaM/TacticM, but it would super helpful to get pointed in the right direction of what goal manipulation functions to use.

[Malcolm Langfield]

Or if this info is in the metaprogramming book, where to look!

[Mario Carneiro]

I think you can do this using docs#Lean.Core.transform to change the expression and docs#Lean.MVarId.replaceTargetDefEq to apply the replacement to the target

[Tomas Skrivan]

Here is a tactic that unfolds a let binding using docs#Lean.Expr.replace

import Lean

open Lean Elab Tactic Conv

syntax (name := let_unfold) " let_unfold " ident : conv

def letUnfold (e : Expr) (id : Name) : Expr :=
  e.replace λ e =>
    if e.isLet && e.letName! = id then
      some (e.letBody!.instantiate1 e.letValue!)
    else
      none

@[tactic let_unfold]
def convLetUnfold : Tactic
| `(conv| let_unfold $id:ident) => do
  (← getMainGoal).withContext do
    let lhs ← getLhs

    changeLhs (letUnfold lhs id.getId)
| _ => Lean.Elab.throwUnsupportedSyntax

macro " let_unfold " id:ident : tactic => `(tactic| conv => let_unfold $id)


def f (n : Nat) : Nat :=
  let n₁ := n + 1
  let n₂ := n₁ + 1
  n₂

example : f 2 = 4 := by
  unfold f
  conv =>
    lhs
    let_unfold n₁

[Malcolm Langfield]

Oh my gosh, wow! Thanks very much @Tomas Skrivan.

[Kyle Miller]

This doesn't do exactly what you asked for, but maybe it's worth considering:

import Mathlib.Tactic

def f (n : Nat) : Nat :=
  let n₁ := n + 1
  let n₂ := n₁ + 1
  n₂

example : f 2 = 4 := by
  unfold f
  lift_lets
  /-
  ⊢ let n₁ := 2 + 1;
    let n₂ := n₁ + 1;
    n₂ = 4
  -/
  intro n₁
  unfold_let n₁
  /-
  ⊢ let n₂ := 2 + 1 + 1;
    n₂ = 4
  -/

[Kyle Miller]

@Tomas Skrivan Is docs#Lean.Expr.replace safe to use here? What if the let value contains bound variables? Experimentally it seems to work, so instantiate1 must be updating bvars in the substituted expression, which I never realized it did.

[Kyle Miller]

Here's another for zeta reducing outermost lets in an expression.

import Mathlib.Tactic

def f (n : Nat) : Nat :=
  let n₁ := n + 1
  let n₂ := n₁ + 1
  n₂

open Lean Elab Tactic in
/--
Zeta reduce the outermost `let` bindings in an expression.
-/
elab "zeta1" : tactic => liftMetaTactic1 fun g => do
  let ty ← g.getType
  let ty' ← Core.transform ty
    (pre := fun e =>
      if e.isLet then
        return .done <| e.letBody!.instantiate1 e.letValue!
      else
        return .continue)
  g.replaceTargetDefEq ty'

example : f 2 = 4 := by
  unfold f
  zeta1
  /-
  ⊢ (let n₂ := 2 + 1 + 1; n₂) = 4
  -/

(I used Core.transform rather than Meta.transform because apparently instantiate1 handles bvars better than I thought it did.)

[Tomas Skrivan]

Kyle Miller said:

Tomas Skrivan Is docs#Lean.Expr.replace safe to use here? What if the let value contains bound variables? Experimentally it seems to work, so instantiate1 must be updating bvars in the substituted expression, which I never realized it did.

I always get confused by bound variables. I think instantiate1 has to update bvars in the body not the value, no? It should not do anything to bvars in the value.

[Kyle Miller]

Consider

def f (n : Nat) : Nat → Nat :=
  let n₁ := n + 1
  let n₂ := n₁ + 1
  fun x => n₂

and doing let_unfold n₂. The value for n₂ is bvar0 + 1, and if you substituted that directly you'd get let n₁ := n + 1; fun x => x + 1, which is incorrect. Instead it seems to see that it's going into one level of bvar depth inside that fun and bumps up the bvar index to actually substitute in bvar1 + 1 so that it refers to n₁.

[Tomas Skrivan]

Ohh I missed that!

[Kyle Miller]

This appears to be one of the C++-implemented functions. This line calls lift_loose_bvars, which I haven't looked at yet, but I'd guess it's doing this bvar bumping.

[Kyle Miller]

This is good to know about instantiate1. I'll put it on my todo list to write a docstring for it!

[Kyle Miller]

(@Tomas Skrivan lean4#3183. It'd be nice to get some feedback on the new docstrings. These functions are a little tricky to explain.)