coqcoq-tactic

Split multiple conjuncts in the goal

Is there a tactic to split multiple conjuncts in a goal into subgoals? If I have the goal P /\ Q /\ R, I want to split it to produce three subgoals at once: P, Q, and R I can't seem to find any info on this.

Solution

  • You can chain tactics. Split twice to split into 3.

    (* Goal P /\ Q /\ R *)

split; [|split].

(* 3 subgoals:
   - P
   - Q
   - R
*)