如何在 Coq 中从见证人那里引入新的存在条件？

Posted 2023-03-29

【中文标题】如何在 Coq 中从见证人那里引入新的存在条件？

【英文标题】：How to introduce a new existential condition from a witness in Coq?

【发布时间】：2015-10-15 05:17:12

【问题描述】：

我的问题与如何在一组条件/假设中构造 exist 术语有关。

我有以下中间证明状态：

X : Type
P : X -> Prop
H : (exists x : X, P x -> False) -> False
x : X
H0 : P x -> False
______________________________________(1/1)
P x

在我的脑海中，我知道因为H0，x是(exists x : X, P x -> False)的见证人，我想介绍一个名字：

w: (exists x : X, P x -> False)

基于以上推理，再与apply H in w一起使用，在假设中生成False，最后inversionFalse。

但我不知道使用什么策略/语法来介绍上面的见证人w。到目前为止我能达到的最好的结果是Check (ex_intro _ (fun x => P x -> False) x H0)). 给了False。

有人可以解释如何引入存在条件，或另一种方法来完成证明吗？

谢谢。

附：我要证明整个定理的是：

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  unfold excluded_middle. unfold not. 
  intros exm X P H x.

  destruct (exm (P x)).
    apply H0.
    Check (H (ex_intro _ (fun x => P x -> False)  x H0)).

【问题讨论】：

请注意，不需要unfold excluded_middle 或not 来使用它们。

【参考方案1】：

在这里，由于您已经知道如何构造 False 类型的术语，因此可以使用 pose proof 将其添加到上下文中。这给出了：

pose proof (H (ex_intro (fun x => P x -> False)  x H0))

你甚至可以直接破坏术语，从而解决了目标。

destruct (H (ex_intro (fun x => P x -> False)  x H0))

完成证明的另一种方法是证明False。您可以使用exfalso 或contradiction 等策略将目标更改为False。通过这种方法，您可以使用_ -> False 形式的假设，否则这些假设很难操作。为了你的证明，你可以写：

exfalso. apply H. (* or directly, contradiction H *)
exists x. assumption.

【讨论】：

谢谢。这很有趣，因为我尝试了induction (H (ex_intro _ (fun x => P x -> False) x H0))，但没有成功。你能解释一下为什么destruct 在这里工作吗？

实际上，它对我有用。也许这是由于您使用的下划线。 ex_intro 需要 4 个参数，但第一个是隐式的，所以不需要指定。我将编辑我的答案。但我不明白为什么它会为你通过类型检查。

我的错，我尝试inversion（不是induction）尝试inversionFalse。但它没有用。你知道为什么destruct/induction 有效而inversion 无效吗？

它也适用于我。在pose proof (H (ex_intro (fun x => P x -> False) x H0)) 之后，inversion H1 解决了目标。你试图反演什么？请注意，您必须反转 False 类型的假设，而不是 False 本身。

谢谢。我可能反转了 False 而不是它的证据。

【参考方案2】：

您可以使用assert 策略：

assert(w: exists x, P x -> False).

它将要求您在新的子目标中证明此陈述，并将w 添加到您现有的目标中。对于这种琐碎的证明，可以直接内联证明：

assert(w: exists x, P x -> False) by (exists x; exact H0).