Reverse unfold

Stream: new members

[Duncan Skahan]

If I was to define e.g. let x := 37, is there a tactic that would change 37 to x in the goal?

[Yaël Dillies]

Does change x to 37 work? That would be my guess

[Duncan Skahan]

Yes. That looks useful.

[Damiano Testa]

You can probably also use set instead of let (and set ... with h to get the equality as an extra assumption).

[Kyle Miller]

example (a : Nat) : 37 = a := by
  let x := 37
  refold_let x
  -- ⊢ x = a

[Kyle Miller]

What's change _ to _ @Yaël Dillies ?

[Luigi Massacci]

(you can also use set and add a with th_name clause after to get the theorem you want in the context)

[Duncan Skahan]

Actually this doesn't quite work for what I'm doing because my definition is a function and it is passed bound variables in the goal.

Yaël Dillies said:

Does change x to 37 work? That would be my guess

[Yaël Dillies]

Kyle Miller said:

What's change _ to _ Yaël Dillies ?

Did I dream the syntax? I definitely remember a change _ to _ or change _ with _ syntax (maybe in Lean 3?) that would target a subexpression rather than the entire goal

[Kyle Miller]

Yes, you seem to be dreaming :-) Lean 3 did have change _ with _ though, and there's an issue tracking it's non-existence: lean4#5116