在目标中拆分多个连词

Question

是否有一种策略可以将一个目标中的多个连接词拆分为子目标？ 如果我有目标 P /\ Q /\ R，我想将其拆分以一次产生三个子目标： P、Q 和 R 我似乎找不到任何这方面的信息。

Answer 1

你可以连锁战术。分割两次即可分割成3份。

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

split; [|split].

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