.. _tac_cases:

cases
=====

Summary
-------

``cases`` is a general-purpose tactic for "deconstructing" hypotheses. If ``h`` is a hypothesis which somehow "bundles up" two pieces of information, then ``cases h with h1 h2`` will make hypothesis ``h`` vanish and will replace it with the two "components" which made the proof of ``h`` in the first place.

Examples
--------

1) The way to make a proof of ``P ∧ Q`` is to use a proof of ``P`` and a proof of ``Q``. If you have a hypothesis ``h : P ∧ Q``, then ``cases h`` will delete the hypothesis and replace it with hypotheses ``h_left : P`` and ``h_right : Q``. These are not the best names for hypotheses; better to type ``cases h with hP hQ``.

2) The way to make a proof of ``P ↔ Q`` is to prove ``P → Q`` and ``Q → P``. So faced with ``h : P ↔ Q`` one thing you can do is ``cases h with hPQ hQP`` which removes ``h`` and replaces it with ``hPQ: P → Q`` and ``hQP: Q → P``. Note however that this might not be the best way to proceed; whilst you can ``apply hPQ`` and ``hQP``, you lose the ability to rewrite ``h`` with ``rw h``. If you really need to keep a copy of ``h`` around, you could always try ``have h2 := h, cases h with hPQ hQP``.

3) There are two ways to make a proof of ``P ∨ Q``. You either use a proof of ``P``, or a proof of ``Q``. So if ``h : P ∨ Q`` then ``cases h with hP hQ`` has a different effect to the first two examples; after the tactic you will be left with *two* goals, one with a new hypothesis ``hP : P`` and the other with ``hQ : Q``. One way of understanding why this happens is that the :ref:`inductive type <ind_types>` ``or`` has two constructors, whereas ``and`` only has one.

4) There are two ways to make a natural number ``n``. Every natural number is either ``0`` or ``succ(m)`` for some natural number ``m``. So if ``n : ℕ`` then ``cases n with m`` gives two goals; one where ``n`` is replaced by ``0`` and the other where it is replaced by ``succ(m)``. Note that this is a strictly weaker version of the ``induction`` tactic, because ``cases`` does not give us the inductive hypothesis.

5) If you have a hypothesis ``h : ∃ a, a^3 + a = 37`` then ``cases h with x hx`` will give you a number ``x`` and a proof ``hx : x^3 + x = 37``.

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

Note that ``∧`` is right associative: ``P ∧ Q ∧ R`` means ````P ∧ (Q ∧ R)``. So if ``h : P ∧ Q ∧ R`` then ``cases h with h1 h2`` will give you ``h1 : P`` and ``h2 : Q ∧ R`` and then you have to do ``cases h2`` to get to the proofs of ``Q`` and ``R``. The syntax ``cases h with h1 h2 h3`` doesn't work (``h3`` just gets ignored). A more refined version of the ``cases`` tactic is the ``rcases`` tactic (although the syntax is slightly different; you need to use pointy brackets ``⟨,⟩`` with ``rcases``). For example if ``h : P ∧ Q ∧ R`` then you can do ``rcases h with ⟨hP, hQ, hR⟩``.