What's the difference between rewrite and rw?

Stream: new members

[Andreas Gittis]

Very silly question I'm sure. I assumed these were the same thing, and the documentation (https://lean-lang.org/theorem_proving_in_lean4/tactics.html#basic-tactics) says that they are. I couldn't google anything about them being different. However here are two proofs:

example (a b c : Nat)
  : a + b + c = a + c + b := by
  rw [add_assoc]
  rw [add_comm b]
  rw [←add_assoc]

example (a b c : Nat)
  : a + b + c = a + c + b := by
  rewrite [add_assoc]
  rewrite [add_comm b]
  rewrite [←add_assoc]

The first one type-checks, the second leaves this goal:

⊢ a + c + b = a + c + b

It can be closed by rfl of course, but are rw and rewrite not interchangeable? If I go through a proof and replace every 'rewrite' with 'rw', are there any risks? Thanks.

[Richard Copley]

Not the same in Lean 4 - hover over rw in VS code for the explanation.

If I go through a proof and replace every 'rewrite' with 'rw', are there any risks? Thanks.

They mean different things, so my suggestion is to use the one you mean. (But some people do use rw everywhere. That wastes a very little CPU time, but nothing more serious.)

[Patrick Massot]

See https://github.com/leanprover/lean4/blob/06e057758e3d63f286b023e3f6ef0468d7b0441e/src/Init/Tactics.lean#L365-L373

[Andreas Gittis]

Okay I see, thanks!