split

split is primarily used to break a single goal of the form A /\ B into two new goals A and B.

You will often notice that split seems to solve some of the subgoals that it generates. This is because split is just shorthand for constructor 1 (see the constructor tactic).

Looking at the definition of /\ (or and):

Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B.

we can see that and has a single constructor called conj - so constructor 1 simply reduces to apply conj, which would give us goals A and B due to the impliciations that it carries.

Syntax

split.

Examples

Before

=========================
1/1
True /\ False

split.

After

=========================
1/2
True
=========================
2/2
False

Resources

Reference Documentation

---