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 inductive type 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⟩.