.. _tac_rw: rw == Summary ------- The ``rw`` or ``rewrite`` tactic is a "substitute in" tactic. If ``h : x = y`` is a hypothesis then ``rw h`` changes all of the ``x``s in the goal to ``y``s. ``rw`` also works with iff statements: if ``h : P ↔ Q`` then ``rw h`` will replace all the ``P``s in the goal by ``Q``s. ``rw`` works up to syntactic equality, and only works with ``=`` and `` Examples -------- 1) Faced with .. code-block:: h : x = y ⊢ x ^ 2 = 1369 the tactic ``rw h`` will turn the goal into ``y ^ 2 = 1369``. 2) ``rw`` works with ``↔`` statements as well. Faced with .. code-block:: h : P ↔ Q ⊢ P ∧ R the tactic ``rw h`` will turn the goal into ``⊢ Q ∧ R``. 3) ``rw`` can also be used to rewrite in hypotheses. For example given ``h : x = y`` and ``h2 : x ^ 2 = 289``, the tactic ``rw h at h2`` will turn ``h2`` into ``h2 : y ^ 2 = 289``. You can rewrite in multiple places at once -- for example ``rw h at h1 h2 h3`` will change all occurrences of the left hand side of ``h`` into the right hand side, in all of ``h1``, ``h2`` and ``h3``. If you want to rewrite in a hypothesis and a goal at the same time, try ``rw h at h1 ⊢`` (type the turnstile ``⊢`` symbol with ``\|-``). 4) ``rw`` doesn't just eat hypotheses -- the theorem ``zero_add`` says ``∀ x, 0 + x = x``, so if you have a goal `` ⊢ 0 + t = 37`` then ``rw zero_add`` will change it to ``t = 37``. Note that ``rw`` is smart enough to fill in the value of ``x`` for you. 5) If you want to replace the right hand side of a hypothesis ``h`` with the left hand side, then ``rw ← h`` will do it. Type ``←`` with ``\l``, noting that ``l`` is a small letter ``L`` for left, and not a number ``1``. 6) You can chain rewrites in one tactic. Equivalent to ``rw h1, rw h2, rw h3`` is ``rw [h1, h2, h3]``. 7) ``rw`` will match on the first thing it finds. For example, ``add_comm`` is the theorem that ``∀ x y, x + y = y + x``. If the goal is ``⊢ a + b + c = 0`` then ``rw add_comm`` will change it to ``⊢ c + (a + b) = 0``, because if we strip away the notation then ``a + b + c = add (add a b) c``, which gets changed to ``add c (add a b)``. If you wanted to switch ``a`` and ``b`` then you can tell Lean to do this explicitly with ``rw add_comm a b``. Further notes ------------- 1) ``rw`` tries a weak version of ``refl`` when it's finished. Beginners can find this confusing; indeed I disabled this in the natural number game because users found it confusing. As an example, if your tactic state is .. code-block:: h : P ↔ Q ⊢ P ∧ R ↔ Q ∧ R then ``rw h`` will close the goal, because after the rewrite the goal becomes ``⊢ Q ∧ R ↔ Q ∧ R`` and ``refl`` closes this goal. 2) A variant of ``rw`` is ``rwa``, which is ``rw`` followed by the ``assumption`` tactic. For example if your tactic state is .. code-block:: h1 : P ↔ Q h2 : Q ↔ R ⊢ P ↔ R then ``rwa h1`` closes the goal, because it turns the goal into ``Q ↔ R`` which is one of our assumptions. 3) If ``h : x = y`` and your goal is ``⊢ x * 2 + z = x``, then ``rw h`` will turn *both* ``x``s into ``y``s. If you only want to turn one of the ``x``s into a ``y`` then you can use ``nth_rewrite 0 h`` (for the first one) or ``nth_rewrite 1 h`` (for the second one). 4) ``rw`` works up to :ref:`syntactic equality `. This means that if ``h : (P → false) ↔ Q`` and the goal is ``⊢ ¬P`` then ``rw h`` will fail, even though ``P → false`` and ``¬P`` are definitionally equal. The left hand side has to match *on the nose*. 5) ``rw`` does not work under binders. Examples of binders are ``∀`` and ``∃``. For example, if your goal is ``⊢ ∀ (x : ℕ), x + 0 = 0 + x`` then ``rw add_zero`` will not work. In situations like this you need to use the more powerful ``simp_rw`` tactic; ``simp_rw add_zero`` works and changes the goal to ``∀ (x : ℕ), x = 0 + x``.