.. _tac_by_contra:

by_contra
=========

Summary
-------

The ``by_contra`` tactic is a "proof by contradiction" tactic. If your goal is ``⊢ P`` then ``by_contra h`` introduces a hypothesis ``h : ¬P`` and changes the goal to ``false``.

Example
-------

Here is a proof of ``¬ ¬ P → P``.

.. code-block::

   example (P : Prop) : ¬ ¬ P → P :=
   begin
     intro hnnP, -- assume ¬ ¬ P
     by_contra hnP, -- goal is now false
     apply hnnP, -- goal is now ¬ P
     exact hnP,
   end

Make a new Lean file in a Lean project and cut and paste the above code into it. See if you can understand the logic.

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

The ``by_contra`` tactic is strictly stronger than the ``exfalso`` tactic in that not only does it change the goal to ``false`` but it also throws in an extra hypothesis. However ``exfalso`` often terminates in under a millisecond, a speed which ``by_contra`` can only dream of.