主页 / coding / 问题 / 79597336
Accepted
Arthur Kexu-Wang
Asked: 2025-04-29 05:54:38 +0800 CST

在 Coq（或 Rocq）中，具有全称结论的引理不能应用于其他前提吗？

  • 772

当我用 Coq（或 Rocq）证明时，我发现有时如果一个假设是“P”而另一个假设是“P -> forall x, Q x”，我无法通过肯定前件将“forall x, Q x”变成一个新的前提。

以下是一个例子：

Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
  (P -> forall x, Q x) -> forall x, P -> Q x.
Proof.

(* 
Here is a correct proof:

intros X P Q. 
intros H.
intros y.
intros H1.
generalize dependent y.
apply H.
apply H1. 
Qed.
*)


intros X P Q. 
intros H.
intros y.
intros H1.
generalize dependent y.
apply H in H1.
(** STUCK HERE, 

But Why cannot we do this???

They look the same.
*)
Admitted.

证明将停留在“在 H1 中应用 H”这一行，并且 Coq 返回“无法找到变量 x 的实例”。

但是“x”必须被实例化吗？这看起来没有必要。这两个证明有什么区别？

我咨询了DeepSeek和ChatGPT，但他们都没能给出令人满意的答案。

我还猜测这可能是先行句中变量出现的问题。但如果是这样，“泛化依赖”策略应该会失败。

logic

3 个回答

  1. 请参阅文档：一个简单的解决方法是使用eapply H in H1，或者仅用 来结束证明exact (H H1)。

    或者，请注意，您在这里实际上并不需要策略：整个证明只是fun X P Q H x p => H p x。

    • 0
  2. Best Answer

    您正在寻找的行为是可用的，但您需要使用specialize策略，它将取代您的暗示而不是您的后果[参考]。

    省略了一些证明内容的示例：

    H : P -> (forall x : X, Q x)
H1 : P
______________________________________(1/1)
False

    specialize (H H1)

    H : forall x : X, Q x
H1 : P
______________________________________(1/1)
False

    我也很困惑，我觉得你发现了“应用”中的一个怪癖。我在旧版本的其他功能中也看到过类似的内部量化推理限制。（具体来说，是在 CPDT 中，如果有人还记得的话……）

    • 0

  3. 模块 pones 是A => B，这里是(forall x, A -> B x) => (A => forall x, B x）。这不一样。当然模块开头暗示了这一点，但不能直接应用。如果要使用模块 pones，必须先引入所有变量。

    Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
  (P -> forall x, Q x) -> forall x, P -> Q x.
Proof.
  intros X P Q Hpq x p. apply Hpq. exact p.
Qed.
    • -1

相关问题