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

Question

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

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

如何证明？

Answer 1

你不能，因为 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.