Rewrite local `let` definitions

Stream: new members

[Gareth Ma]

example : True := by
  let c : ℕ → ℕ := fun x => x
  have h {x : ℕ} : c (x + 1) = x + 1 := by
    /- rw [c] -/
    /- dsimp [c] -/
    simp -- this works

What's the correct way to do this?

[Gareth Ma]

Something stupid like this also works:

example : True := by
  let c : ℕ → ℕ := fun x => x
  have h {x : ℕ} : c (x + 1) = x + 1 := by
    rw [show c = fun x => x by rfl]

[Gareth Ma]

To make it closer to my scenario:

example : True := by
  let f : ℕ → ℕ := fun x => x
  let g : (ℕ → ℕ) → (ℕ → ℕ) := fun y => (fun x => Nat.floor ((cos (sin ↑x)) ^ 2 / 5)) -- complicated things
  have h : g (fun x => 2 * f x) = g (fun x => x * 2) + g (fun _ => 0) := by
    dsimp only [f] -- ??

I don't want to expand g's definition because it's quite complicated. I want to expand f first so that f x gets replaced with x, but I can't figure out a way to do that.

[Timo Carlin-Burns]

It seems a little annoying to rewrite using the definitions of lets compared to top-level declarations... The reason rw [f] would work if you had def f := ... is because of a feature called "equational lemmas", where a lemma theorem f._eq_ (n : ℕ) : f n = n is generated alongside your definition which rw and simp automatically look for when you try rw [f].

[Timo Carlin-Burns]

I wonder if there's a tactic which generates a hypothesis that a let equals its definition. So here hf : \all n, f n = n

[Timo Carlin-Burns]

if you want f to be expanded everywhere, I think you could try letI f instead of let f. The I stands for "inline" and it automatically substitutes the definition of f inline whenever it is referenced

[Timo Carlin-Burns]

ah! maybe unfold_let would work?

[Gareth Ma]

Oh wow, yes unfold_let works perfectly, thanks.

[Alex J. Best]

You can also use set a := 1 with h to get a named hypothesis which is helpful

[Gareth Ma]

Ah, that's how to do the "equational lemma" thing then.

[Timo Carlin-Burns]

I just tested letI and it didn't seem to make a difference so I guess it doesn't do what I thought :shrug:

[Chris Wong]

I thought letI was about instances?

[Chris Wong]

Ah, they changed it from Lean 3 to 4 :sweat_smile:

[Gareth Ma]

Another related question, is funext within conv removed in Lean 4? Or not ported?

[Gareth Ma]

Is there any way to rewrite this in Lean 4?

example : (fun x => x + 0) = (fun x => x) := by
  -- rw [add_zero] -- fails
  conv =>
    lhs
    funext -- fails
    rw [add_zero]
  rfl

[Timo Carlin-Burns]

looks like ext instead of funext works?

[Gareth Ma]

Oh thanks a lot

[Gareth Ma]

That will save me a lot of time :sweat_smile:

[Timo Carlin-Burns]

simp_rw [add_zero] also works if the challenge is rewriting under binders

[Gareth Ma]

Oh so simp_rw goes inside binders as well

[Gareth Ma]

Nice. I finally proved my result after like a few hours..

[Eric Wieser]

To turn off this "expand all lets" behavior, you can use dsimp (config := { zeta := false }) only [f] which will not unfold g

[Eric Wieser]

There is a thread somewhere petitioning to make this the default

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20unfolding.20let.20bindings

[Eric Rodriguez]

Should I just open a core lean4 issue?

[Eric Rodriguez]

lean4#2682