tactic to re-replace let-bound terms

Stream: lean4

[Jakob von Raumer]

Is there a tactic somewhere which reapplies all let-bindings to the goal and to other hypothesis, i.e. if I have foo : T := bar 1 2 3 in the context, replacing each occurrence of bar 1 2 3 by foo?

[Markus Himmel]

It's not exactly what you're asking for, but the set tactic does the let binding and the replacement in one step:

import Mathlib

theorem bla {x : ℕ} (hx : 5 = x) : 5 = 5 := by
  set y := 5

/-
x: ℕ
y: ℕ := 5
hx: y = x
⊢ y = y
-/

[Jakob von Raumer]

Yea, I know set, but my let bindings get introed because they appear in the goal and then later on I want to apply them in other hypotheses

[Jakob von Raumer]

How do I re-fold let bindings at all? Unfolding works with rw but, contrary to definitions, I cant use ← on them inside rw or simp...

[Markus Himmel]

The set tactic just does rw [(show bar 1 2 3 = foo from rfl)] at *

[Yaël Dillies]

You use change :grimacing:

[Jakob von Raumer]

Yaël Dillies said:

You use change :grimacing:

Mhhh, big goal :sweat_smile:

[Yaël Dillies]

Keep your goals big and your dreams even bigger :punch:

[Jakob von Raumer]

Guess I should just write my own tactic for that stuff, then tidy_let or so...

[Ruben Van de Velde]

You can do have hx : x = ... := rfl and rewrite with that

[Jakob von Raumer]

True, but that means for each of my let-bindings doing

have hx : x = ... := rfl
subst hx
clear hx

which is quite a bit unwieldy... but maybe that's exactly how I should implement said automated tactic

[Yaël Dillies]

Wait why subst hx? That undoes the binding

[Markus Himmel]

How would that work? Doesn't subst do the exact opposite of what you want?

[Jakob von Raumer]

Ah I meant simp only [← hx] at *

[Jakob von Raumer]

* isn't right either because it includes hx itself, it's supposed to rewrite everwhere except for hx...

example (h : x = 6 - 1) : let y := 6; x = y - 1 := by
  intro y
  have hy : y = 6 := rfl
  rw [← hy] at h
  clear hy
  assumption

[Yaël Dillies]

In Lean 3, rw [h] at h was a no-op

[Markus Himmel]

I don't see what introducing the hypothesis gains you over the direct way

example (h : x = 6 - 1) : let y := 6; x = y - 1 := by
  intro y
  rw [show 6 = y from rfl] at *
  assumption

[Ruben Van de Velde]

You might want to use the hypothesis more than once or in a more targeted way

[Jakob von Raumer]

@Markus Himmel Nothing, I guess, you're right

[Jakob von Raumer]

I guess I will really write a tactic... The body of the let bindings contain lots of :cross:'ed variables, so stating their body explicitly is also not good

[Kyle Miller]

@Jakob von Raumer I just created #12745 for refold_let

[Jakob von Raumer]

Will test it tomorrow!