Coq中不拆分合取分支应用引理实现C∧B目标的方法问询

首先得明确核心逻辑：你的引理C → A本质是帮你把「证明A」的任务转化为「证明C」。要把原目标A ∧ B转化为C ∧ B，其实是利用**C ∧ B → A ∧ B**这个蕴含关系——只要能证出C ∧ B，结合C→A，自然能推出A ∧ B。下面分两种常见场景讲具体实现（以Coq为例，这是这类问题最常用的交互式证明器）：

场景1：直接把目标切换成C ∧ B #

如果你想一步到位把原目标A ∧ B替换成C ∧ B，可以用匿名函数构造证明项的方式，直接告诉证明器如何从C ∧ B推导出A ∧ B：

(* 假设已有引理L : C → A，当前目标是A ∧ B *)
apply (fun H : C ∧ B => conj (L (proj1 H)) (proj2 H)).

这段代码的意思是：定义一个函数，输入C ∧ B的证明H，用引理L把H里的C转换成A，再和H里的B组合成A ∧ B的证明。执行完这个战术，你的目标就会变成C ∧ B，接下来只要证明这个新目标就行。

要是你觉得匿名函数太繁琐，也可以先单独证明这个蕴含引理，再复用：

Lemma c_b_to_a_b : C ∧ B → A ∧ B.
Proof.
  intros H. split.
  - apply L. apply (proj1 H).
  - apply (proj2 H).
Qed.

(* 之后直接用 *)
apply c_b_to_a_b.

场景2：split后处理子目标（你提到的方法） #

你说的「split后对第一个子目标应用引理」完全可行，而且不需要额外“重新组合”C和B——因为split本身就是把A ∧ B拆成A和B两个独立子目标，当你把A的子目标换成C并证明后，Coq会自动把两个子目标的结果组合回A ∧ B。步骤如下：

(* 当前目标：A ∧ B *)
split.
(* 现在得到两个子目标：A 和 B *)
- (* 处理第一个子目标A *)
  apply L. (* 因为L是C→A，所以目标直接变成C *)
  (* 这里补全C的证明 *)
- (* 处理第二个子目标B *)
  (* 这里补全B的证明 *)

等你完成C和B的证明，Coq会自动帮你把它们拼成A ∧ B的最终证明——这和直接证明C ∧ B再推导A ∧ B是逻辑等价的，只是战术路径不同。

关于apply能否作用于合取的单个分支 #

你观察到的「apply无法直接作用于合取的单个分支」是对的——默认情况下，apply是作用于整个目标的。但我们可以通过两种方式间接实现对单个分支的修改：

1. 先用split拆分合取目标，得到独立的子目标后，再对单个分支用apply（就是上面场景2的方法）。
2. 用apply结合组合式证明项，比如：

(* 当前目标：A ∧ B *)
apply (conj (L _) _).

这会让Coq自动生成两个子目标：C（对应L需要的输入）和B，效果和split后apply L完全一致。

关键提醒 #

这种转换有个前提：你必须能证明C。因为C→A只是说C能推出A，但如果C本身不成立，那C ∧ B根本证不出来，自然也推不出A ∧ B。要是原目标A ∧ B是成立的，但C不成立，那这种转换就会走进死胡同，这点一定要注意。

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