split
Summary
If your goal is a proof which is “made up of subproofs” (for example a goal like
⊢ P ∧ Q
; to prove this you have to prove P
and Q
) then the split
tactic will turn your goal into these multiple simpler goals.
Examples
Faced with the goal
⊢ P ∧ Q
, thesplit
tactic will turn it into two goals⊢ P
and⊢ Q
.Faced with the goal
⊢ P ↔ Q
,split
will turn it into two goals⊢ P → Q
and⊢ Q → P
.Something which always amuses me – faced with
⊢ true
,split
will solve the goal. This is becausetrue
is made up of 0 subproofs, sosplit
turns it into 0 goals.
Further notes
The refine
tactic is a more refined version of split
; faced with a goal of ⊢ P ∧ Q
, split
does the same as refine ⟨_, _⟩,
. In fact refine
is more powerful than split
; faced with ⊢ P ∧ Q ∧ R
you would have to use split
twice to break it into three goals, whereas refine ⟨_, _, _⟩
does the job in one go.