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)¶
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.
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)¶
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 (∃)¶
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.