Search code examples
coqproof

Prove that one hypothesis is negation of another in Coq

For example I have these two hypotheses (one is negation of other)

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

And goal

False

How to prove it?

Solution

  • You can't, because H0 is not the negation of H. The correct statement would be

    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.