在 Coq 的另一个子目标中使用经过验证的子目标

Question

假设我想证明P : A -> (B /\ C)。在intros. split. 之后，Coq 生成两个子目标，我分别证明B 和C，以A 为前提。假设我已经证明了第一个子目标并进入了第二个子目标。有什么方法可以引入先前证明的子目标，以便我在上下文中有B？

一种明显的方法是将原始定理重构为P1 : A -> B 和P2 : A -> C，但如果我能跳过那部分就好了，尤其是在进行紧凑的自动证明时。

Answer 1

您可以在split. 之前assert B. 并证明它，然后split 并使用假设证明B，然后继续证明C 与B 可用。

或者，您可以构建一个：

Theorem and_intro_2 :
  forall A B C : Prop,
    (A -> B) ->
    (A -> B -> C) ->
    A -> B /\ C.
Proof. firstorder. Qed.

并在开始时立即应用。