Defining a new term

Stream: new members

[Wojtek Wawrów]

This is probably very basic but I'm having trouble finding something for it. Suppose I have a long term like a+b+c+d and I want to introduce a new name, say n, for use of it in a proof. How would I do that? I thought have would be the obvious answer but it doesn't seem to give me any sort of assumption like n=a+b+c+d which I could then rewrite with.

[Heather Macbeth]

@Wojtek Wawrów You can use let n := a + b + c + d, and then, when you need to look under the hood, use rw n to replace n with a + b + c + d.

[Heather Macbeth]

The difference between let and have is precisely what you noticed: have n := a + b + c + d forgets how n was defined.

[Wojtek Wawrów]

That's perfect, thank you!

[Adam Topaz]

We also have the (essentially equivalent) tactic called tactic#set with the syntax being set n := a + b + c + d with hn which will introduce an assumption hn : n = a + b + c + d into context.

[Wojtek Wawrów]

@Heather Macbeth Actually, rw n doesn't seem to work - I'm getting rewrite tactic failed, lemma is not an equality nor a iff when I try it

[Adam Topaz]

I think dsimp [n] should work.

[Adam Topaz]

Maybe unfold n? (or delta n)

[Wojtek Wawrów]

dsimp works, but neither unfold nor delta seems to. I think I will go with set .. with ... solution (rewriting using the given name works)

[Martin Dvořák]

Heather Macbeth said:

The difference between let and have is precisely what you noticed: have n := a + b + c + d forgets how n was defined.

Wow, thank you! This resolved a lot of my confusion.