gpt4 book ai didi

coq - 在 Coq 中证明一个假设是另一个假设的否定

转载 作者:行者123 更新时间:2023-12-04 14:09:15 27 4
gpt4 key购买 nike

例如我有这两个假设(一个是另一个的否定)

H : forall e : R, e > 0 -> exists p : X, B e x p -> ~ F p
H0 : exists e : R, e > 0 -> forall p : X, B e x p -> F p

目标

False

如何证明?

最佳答案

你不能,因为 H0 不是 H 的否定。正确的说法是

Definition R := nat.
Parameter X: Type.
Parameter T: Type.
Parameter x: T.
Parameter B : R -> T -> X -> Prop.
Parameter F : X -> Prop.

Lemma foobar: forall (H: forall e : R, e > 0 -> exists p : X, B e x p -> ~ F p)
(H0: exists e: R, e > 0 /\ forall p: X, B e x p /\ F p), False.
Proof.
intros H H0.
destruct H0 as [e [he hforall]].
destruct (H e he) as [p hp].
destruct (hforall p) as [hB hF].
exact (hp hB hF).
Qed.

关于coq - 在 Coq 中证明一个假设是另一个假设的否定,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/32882779/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com