Unfolding local function

Stream: new members

[Felipe]

It seems when using let to declare a function in a block of tactics that rw/simp/unfold don’t work on it. Is there a different tactic needed for that? FWIW, I’m defining a local function to apply an induction principle and need to prove some properties of it. Also, it’s technically a closure

[Junyan Xu]

dsimp only [name_of_your_function] should work. I forgot whether simp only is supposed to work ...

[Matt Diamond]

simp_rw F might also work (where F is the name of your function)

[Martin Dvořák]

Which version of Lean is it for?

[Riccardo Brasca]

Unless it is explicitly said, we always talk about Lean 3 (except in the Lean4 stream of course).

[Martin Dvořák]

I was confused because I never saw simp_rw before.

[Riccardo Brasca]

Here it is.

[Martin Dvořák]

Oh! It looks delicious!

[Riccardo Brasca]

If rw gives the infamous "motive is not type correct" error, then simp_rw is the first thing to try.

[Riccardo Brasca]

It's also very useful to rewrite under binders.

[Felipe]

Thanks! Is there an equivalent in Lean4?

[Alex J. Best]

If you use mathlib4 there is a direct replacement https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/SimpRw.html#Mathlib.Tactic.tacticSimp_rw__

[Felipe]

Thanks. I'm still getting "invalid 'simp', proposition expected" when I do simp_rw [f] at X But I was able to work around by switching to term mode

[Martin Dvořák]

What is f and X in your context?

[Jason Rute]

Is this related to https://proofassistants.stackexchange.com/questions/1846/proving-with-non-structural-recursion-in-lean4? My answer hopefully will get you started, but this group might better help you complete your proof.

[Felipe]

Thank you! Your answer did indeed get me on the right track. Seeing the autogenerated lemmas helped me figure out the issue in the original recursive definition and I was able to fix

[Suryansh Shrivastava]

I have used unfold to expand a function that I have already made. I heard that it is a bad practice to use in the Lean code. So, I was wondering how does one not use unfold?

[Martin Dvořák]

I personally don't mind using unfold in my proofs, but if you want to avoid it, there are several things you can use instead:
show followed by a new goal (that has to be definitionally-equal to the old goal)
dsimp only
add a rfl lemma for your definition and use rw

[Martin Dvořák]

Apart from that, you can often notice that you do unfold and a next step, but if you remove unfold the next step still works.