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.

Example 1 (and)

try it!

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

When this proof begins, the state is

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

After cases H with HP HQ the state is

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.

Example 2 (or)

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

try it!

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

H : P ∨ Q
⊢ true

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

HP : P,
⊢ true

and the second like this:

HP : Q,
⊢ true

Hence trivial needs to be applied twice, once for each goal.

Example 3 (iff)

try it!

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.

Example 4 (∃)

try it!

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.