.. _tactic.cases:

cases
=====

The ``cases`` tactic applies to a *hypothesis*, so is usually run in the form ``cases H`` or ``cases H with H1 H2``. Informally, it breaks up hypothesis ``H`` into its component parts. More formally, if ``H`` is a term whose type is an inductive type ``α``, then ``cases H`` replaces ``H`` with all the ways that ``H`` can be constructed, so the number of new goals is the number of constructors of ``α`` and each new local contexts will have the terms needed for each constructor.

.. _tactic.cases.and:

Example 1 (and)
---------------

.. code-block:: lean

   example (P Q : Prop) (H : P ∧ Q) : P :=
   begin
     cases H with HP HQ,
     exact HP
   end

When this proof begins, the state is

.. code-block:: python

   P Q : Prop,
   H : P ∧ Q
   ⊢ P

After ``cases H with HP HQ`` the state is

.. code-block:: python

   P Q : Prop,
   HP : P,
   HQ : Q
   ⊢ P

with the proof ``H`` of ``P ∧ Q`` replaced with proofs ``HP`` of ``P`` and ``HQ`` of ``Q``. The goal of ``P`` is then closed with ``exact HP``. Note that ``P ∧ Q`` is notation for ``and P Q``, an inductive type with one constructor which takes a proof of ``P`` and a proof of ``Q``.

.. _tactic.cases.or:

Example 2 (or)
--------------

Note that `trivial` is a tactic which proves the true/false statement `true`.

.. code-block:: lean

   example (P Q : Prop) (H : P ∨ Q) : true :=
   begin
     cases H with HP HQ,
     { -- first case
       -- HP : P
       -- ⊢ true
       trivial},
     { -- second case     
       -- HQ : Q
       -- ⊢ true
       trivial},
   end
		
At some point, this code has more than one goal. It is interesting to look at the code in Lean and then to click the cursor around at points between the beginning of `begin` and the end of `end`, to see what the state looks like at each point of the argument.

When this proof begins, the relevant part of the state is

.. code-block:: python

   H : P ∨ Q
   ⊢ true

After ``cases H with HP HQ`` there are now two goals to be solved. The first looks like this:

.. code-block:: python

   HP : P,
   ⊢ true

and the second like this:

.. code-block:: python

   HP : Q,
   ⊢ true

Hence `trivial` needs to be applied twice, once for each goal.
   
.. _tactic.cases.iff:

Example 3 (iff)
---------------

.. code-block:: lean

   example (P Q : Prop) (H : P ↔ Q) : P → Q :=
   begin
     cases H with HPQ HQP,
     exact HPQ
   end
		
Here the ``cases`` tactic turns one hypothesis ``H : P ↔ Q`` into two hypotheses ``HPQ : P → Q`` and ``HQP : Q → P``. The goal is then closed with ``exact HPQ`` because hypothesis ``HPQ`` is a proof of the goal.

.. _tactic.cases.exists:

Example 4 (∃)
---------------

.. code-block:: lean

   example (X : Type) (P Q : X → Prop) (H : ∃ x : X, P x ∧ Q x) : ∃ x : X, P x :=
   begin
     cases H with x Hx,
     cases Hx with HPx HQx,
     existsi x,
     assumption
   end

Here hypothesis ``H`` is the assertion that there exists ``x`` of type ``X`` such that both ``P x`` and ``Q x`` are true. We extract ``x`` with the ``cases H`` command; ``Hx`` is the hypothesi that ``P x ∧ Q x`` is true. We use ``cases`` again to extract a proof ``HPx`` of ``P x``, and we put everything together after that.