是否存在可一次性拆分目标中多个合取式为子目标的战术？

原生解决方案 #

Coq中没有专门的单一步骤战术直接拆分所有合取子目标，但可以用repeat split这个组合战术——它会自动重复执行split操作，直到目标中没有可拆分的合取式，能一次性将P /\ Q /\ R拆分为P、Q、R三个独立子目标。

自定义战术（可选） #

如果需要更语义化的调用方式，可以自定义一个专用战术：

Ltac split_all := repeat split.

之后在证明过程中直接调用split_all即可完成多合取式的一次性拆分。

补充说明 #

无论合取式是扁平结构（P /\ Q /\ R）还是嵌套结构（P /\ (Q /\ R)），上述方法都能直接生成所有底层子目标，无需手动分步操作。

内容的提问来源于stack exchange，提问作者confusedcius