split¶
The split
tactic works on goals such as P ∧ Q
or P ↔ Q
. It breaks up one “compound” goal into one or more simpler goals. More formally, if the goal is a structure, that is, an inductive type with one constructor, split
will turn the goal into goals asking for terms of all the types needed for the constructor.
Example (∧)¶
If the goal is
P Q : Prop,
⊢ P ∧ Q
then split
changes this one goal into two goals, namely
P Q : Prop,
⊢ P
and
P Q : Prop,
⊢ Q
Here is a fully worked example.
example (P Q : Prop) (HP : P) (HQ : Q) : P ∧ Q :=
begin
split,
{ -- first goal is P
exact HP
},
{ -- second goal is Q
exact HQ
}
end