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

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

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/