.. _tac_apply:

apply
=====

.. warning::

   The ``apply`` tactic does *one very specific thing*, which I explain below. I have seen students trying to use this tactic to do all sorts of other things, based solely on the fact that they want to "apply a theorem" or "apply a technique". The English word "apply" has **far more uses** than the Lean ``apply`` tactic. The ``apply`` tactic "argues backwards", using an implication to reduce the goal to something closer to the hypotheses. ``apply h`` is like saying "because of ``h``, it suffices to prove this new simpler thing".

Summary
-------

If your local context is

.. code-block::

   h : P → Q
   ⊢ Q

then ``apply h`` changes the goal to ``⊢ P``.

.. note::

   ``apply h`` will *not work* unless ``h`` is of the form ``P → Q``. It will also *not work* unless the goal is equal to the conclusion of ``h``. You will get an obscure error message if you try using ``apply`` in situations which do not conform to the pattern above.

Mathematically, the ``apply`` tactic does this: We're trying to prove ``Q``. If we know that ``P`` implies ``Q`` then of course it would suffice to prove ``P`` instead, because ``P`` implies ``Q``. So ``apply`` *reduces* the goal from ``Q`` to ``P``. If you like, ``apply`` executes the *last* step of a proof of ``Q``, rather than what many mathematicians would think of as the "next" step. 

If instead of an implication you have an iff statement ``h : P ↔ Q`` then ``apply h`` won't work. You might want to "apply" ``h`` by using the :ref:`rw <tac_rw>` (rewrite) tactic.

Examples
--------

1) If you have a hypothesis which is
   
.. code-block::
   
   h : a ^ 2 = b → a ^ 4 = b ^ 2
   ⊢ a ^ 4 = b ^ 2

then ``apply h`` will change the goal to ``⊢ a ^ 2 = b``.

2) ``apply`` works up to :ref:`definitional equality <defeq>`. For example if your local context is

.. code-block::
   
   h : ¬P
   ⊢ false

then ``apply h`` works and changes the goal to ``⊢ P``. This is because ``h`` is definitionally equal to ``P → false``.

3) The ``apply`` tactic does actually have one more trick up its sleeve: in the situation

.. code-block::

   h : P → Q → R
   ⊢ R

the tactic ``apply h`` will work (even though the brackets in ``h`` which Lean doesn't print are ``P → (Q → R)``), and the result will be two goals ``⊢ P`` and ``⊢ Q``. Mathematically, what is happening is that ``h`` says "if ``P`` is true, then if ``Q`` is true, then ``R`` is true", hence to prove ``R`` is true it suffices to prove that ``P`` and ``Q`` are true.

Further notes
-------------

The :ref:`refine <tac_refine>` tactic is a more refined version of ``apply``. For example, if ``h : P → Q`` and the goal is ``⊢ Q`` then ``apply h`` does the same thing as ``refine h _``.