Unfolding let definition

Stream: new members

[Roberto Pettinau]

Hi everyone! Is it possible to unfold a let definition in Lean4? Here is a simple example:

def test (n: Nat): 0 = 1 :=
  let zero: Nat := 0
  let one: Nat := 1
  by
    have h1: 0 = zero := by rfl;
    rw [h1]
    have h2: 1 = one := by rfl;
    rw [h2]

I would like to somehow be able to change my current goal from zero = one to 0=one, by doing some kind of unfold zero.

I am aware of the existence of dsimp, but that would transform the goal into 0=1

[Kevin Buzzard]

What about dsimp only [zero] or if that doesn't work, I can't quite remember the syntax but something like dsimp (config := {zeta := false}) only [zero]?

[Ayhon]

As a follow up to this question, how can you unfold definitions which come from pattern matching on a let definition?

As an example, consider the following code.

example :=
  let (x,y) := (1, 2)
  let res := 3
  have: res = x + y := by
    simp_wf
    sorry
  ()

With the simp_wf, Lean4 is able to substitute res with 3, but I'm not able to deduce anything from x or y. In the InfoView I also don't get any information about x or y. Is this a current limitation?

I would expect to have something like x: Nat := (1,2).fst and y: Nat := (1,2).snd in the InfoView.

[Kyle Miller]

Yeah, this isn't possible at the moment, since let (x, y) := (1, 2); ... is short for match (1, 2) with | (x, y) => ...

This means that it loses the connection to the original value.

One of the workarounds is to manually write match h : (1, 2) with | (x, y) => ..., since that gives you this h in the local context that you can make use of.

[Ayhon]

This also seems to be the case for definitions in the where clause (example).

example :=
  let res := 3
  have: res = x + y := by
    simp_wf
    sorry
  ()
where x := 1
      y := 2

Are where clauses also syntactic sugar for some other construct? If so, do we know if these plan to be supported?

[Aaron Liu]

example :=
  let rec x := 1
  let rec y := 2
  let res := 3
  have: res = x + y := by
    simp_wf
    sorry
  ()

This modifies the environment in the same way, so maybe where is syntax sugar for let rec?

[Kyle Miller]

Yeah, it's sugar for let rec

[Ayhon]

Kyle Miller said:

Yeah, it's sugar for let rec

And why is let rec not able to be unfolded? Just a current limitation?

[Kyle Miller]

It's because let rec defers creating the auxiliary definitions until everything is elaborated. It's a limitation that I don't expect to see change.

[Kyle Miller]

You can at least use let instead