Zulip Chat Archive

Stream: general

Topic: naming part of the goal


view this post on Zulip Reid Barton (Jan 01 2019 at 21:31):

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,

view this post on Zulip Patrick Massot (Jan 01 2019 at 21:32):

Oh, that's sneaky

view this post on Zulip Patrick Massot (Jan 01 2019 at 21:33):

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

view this post on Zulip Sebastian Ullrich (Jan 01 2019 at 22:02):

omg

view this post on Zulip Patrick Massot (Jan 01 2019 at 22:09):

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

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 22:45):

(deleted)

view this post on Zulip Sebastian Ullrich (Jan 01 2019 at 23:03):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 06:20):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 06:20):

since there is no let_suffices tactic

view this post on Zulip Mario Carneiro (Jan 02 2019 at 06:22):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 06:26):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 06:29):

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

view this post on Zulip Mario Carneiro (Jan 02 2019 at 06:31):

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

view this post on Zulip Johan Commelin (Jan 02 2019 at 08:09):

@Reid Barton That's brilliant!


Last updated: May 15 2021 at 00:39 UTC