2

我的问题与如何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)

基于以上推理,然后用 withapply H in w生成False假设中的 a,最后inversion生成False.

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

有人可以解释如何引入存在条件,或者完成证明的另一种方法吗?

谢谢。

PS我要证明整个定理的是:

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)).
4

2 回答 2

2

您可以使用以下assert策略:

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

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

assert(w: exists x, P x -> False) by (exists x; exact H0).
于 2015-10-15T06:52:52.067 回答
2

在这里,由于您已经知道如何构造一个类型的术语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. 您可以使用或之False类的策略将目标更改为。使用这种方法,您可以使用难以操作的形式假设。为了你的证明,你可以写:exfalsocontradiction_ -> False

exfalso. apply H. (* or directly, contradiction H *)
exists x. assumption.
于 2015-10-15T07:58:04.130 回答