.. _tac_split:

split
=====

Summary
-------

If your goal is a proof which is "made up of subproofs" (for example a goal like
``⊢ P ∧ Q``; to prove this you have to prove ``P`` and ``Q``) then the ``split`` tactic will turn your goal into these multiple simpler goals.

Examples
--------

1) Faced with the goal ``⊢ P ∧ Q``, the ``split`` tactic will turn it into two goals ``⊢ P`` and ``⊢ Q``.

2) Faced with the goal ``⊢ P ↔ Q``, ``split`` will turn it into two goals ``⊢ P → Q`` and ``⊢ Q → P``.

3) Something which always amuses me -- faced with ``⊢ true``, ``split`` will solve the goal. This is because ``true`` is made up of 0 subproofs, so ``split`` turns it into 0 goals.

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

The ``refine`` tactic is a more refined version of ``split``; faced with a goal of ``⊢ P ∧ Q``, ``split`` does the same as ``refine ⟨_, _⟩,``. In fact ``refine`` is more powerful than ``split``; faced with ``⊢ P ∧ Q ∧ R`` you would have to use ``split`` twice to break it into three goals, whereas ``refine ⟨_, _, _⟩`` does the job in one go.