.. _tactic.split:

split
=====

The ``split`` tactic works on goals such as ``P ∧ Q`` or ``P ↔ Q``. It breaks up one "compound" goal into one or more simpler goals. More formally, if the goal is a *structure*, that is, an inductive type with one constructor, ``split`` will turn the goal into goals asking for terms of all the types needed for the constructor.

.. _tactic.split.and:

Example (∧)
------------

If the goal is

.. code-block:: python

   P Q : Prop,
   ⊢ P ∧ Q

then ``split`` changes this one goal into two goals, namely

.. code-block:: python

   P Q : Prop,
   ⊢ P

and

.. code-block:: python

   P Q : Prop,
   ⊢ Q
   
   
Here is a fully worked example.

.. code-block:: lean
		
   example (P Q : Prop) (HP : P) (HQ : Q) : P ∧ Q :=
   begin
     split,
     { -- first goal is P
       exact HP
     },
     { -- second goal is Q
       exact HQ
     }
   end

.. _tactic.split.iff:

Example (↔)
------------

A term of type ``P ↔ Q`` is constructed in Lean by giving terms of type ``P → Q`` and ``Q → P``. 

.. code-block:: lean
		
   example (P Q : Prop) (HPQ : P → Q) (HQP : Q → P) : P ↔ Q :=
   begin
     split,
     { -- first goal is P → Q
       exact HPQ
     },
     { -- second goal is Q → P
       exact HQP
     }
   end