Tactics questions

Stream: new members

[Michael Stoll]

Are there existing tactics doing the following?

• The equivalent of the sequence have subst : a = b := by ring, rw subst, clear subst. I.e., I want to replace a term a in my goal (or some assumption) by b, where a and b are living in a ring and a = b follows from the ring axioms.
• The equivalent of the sequence let x := a, have hx : x = a := by refl, rw ← hx. I.e., I want to introduce an abbreviation x for some term a (say, to hide irrelevant structure).

[Patrick Massot]

rw show a = b, by ring,

[Patrick Massot]

set x := a

[Alex J. Best]

Or rw (by ring : a = b) for the first

[Patrick Massot]

If you really think the term a is irrelevant you can even go as far as generalize : a = x

[Michael Stoll]

@Alex J. Best Thanks! I think I tried something like this, but I probably got the parentheses wrong...

[Michael Stoll]

@Patrick Massot In some cases, that would do, but in others, I will have to go back to the original terms.

[Patrick Massot]

Then you need to remember both answers :smile:

[Patrick Massot]

Compare

example (n : ℕ) : 1 + 1 + n = n + (1+1) :=
begin
  generalize : 1 + 1 = x,
  rw add_comm,
end

example (n : ℕ) : 1 + 1 + n = n + (1+1) :=
begin
  set x := 1 + 1,
  rw add_comm,
end

[Patrick Massot]

(you need to look at the tactic state of course)

[Patrick Massot]

Bonus: you can use set x := 1 + 1 with h, to also create an assumption h : x = 1 + 1

[Michael Stoll]

@Patrick Massot Thanks. I had overlooked your first answer to my second question at first.

[Michael Stoll]

How can I mark the question as solved?

[Patrick Massot]

Please don't. This only generates noise

[Alex J. Best]

I don't think it does anymore? There is a small tick mark next to the title

[Michael Stoll]

Ah, OK, there is a button in the title bar. But I'll refrain from using it for now...

[Alex J. Best]

https://github.com/zulip/zulip/pull/20977 is what I was thinking of, it significantly reduced the noise from this feature imo

[Patrick Massot]

Oh, nice!

[Patrick Massot]

It seems resolving the topic still posts a new message, right?

[Alex J. Best]

Yes, just no notification for people who didnt reply to the thread, so I guess it depends on how you use the zulip feed whether you see them all show up or not

[Michael Stoll]

Then it should be OK to mark the topic as resolved, since it will affect only the two of you?