naming part of the goal

Stream: general

[Reid Barton]

I discovered a trick for referring to parts of the goal without having to write them out. For example, suppose your goal is to prove that some really complicated expression equals 0. You can give that expression a name lhs by writing

  let lhs := _,
  change lhs = 0,

[Patrick Massot]

Oh, that's sneaky

[Patrick Massot]

It could be nice to wrap this trick in a small tactic

[Sebastian Ullrich]

omg

[Patrick Massot]

I can feel this trick won't be allowed in Lean 4...

[Kevin Buzzard]

(deleted)

[Sebastian Ullrich]

@Patrick Massot I don't see anything wrong with any specific part here, it's more like a surprising combination of features

[Mario Carneiro]

you can also use let lhs, swap, which is what I usually use for this trick

[Mario Carneiro]

since there is no let_suffices tactic

[Mario Carneiro]

I think having a tactic for this wouldn't be a bad idea though. Possibly using conv patterns to find the expression to name

[Mario Carneiro]

How about this: name foo + 1 + bar will treat any undefined names in the expression like foo and bar as holes to be filled. It searches for the first unifying subterm of the goal (or hyps) and let binds them and replaces them in the target (not just in the pattern, in the whole goal). So if the goal is (x - 3) + 1 + (y - 3) = x - 3 then the resulting goal is foo := x - 3, bar := y - 3 |- foo + 1 + bar = foo

[Mario Carneiro]

It doesn't work in the presence of binders; or more specifically it won't match any open terms. I don't see what other option is available

[Mario Carneiro]

so if the goal was \exists y, (x - 3) + 1 + y = x - 3 then the inner match (x - 3) + 1 + #0 would be ignored

[Johan Commelin]

@Reid Barton That's brilliant!