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