Question

I have following unfinished proof of a lemma:

Goal forall (P : Type -> Prop) (Q : Prop),
  ((forall x, (P x)) -> Q) -> (exists x, P x -> Q).
Proof.
  intros. 
  eapply ex_intro. intros. apply H. intros. eapply H0.

The problem is the last eapply failed, with the message

Error:
In environment
P : Type -> Prop
Q : Prop
H : (forall x : Type, P x) -> Q
H0 : P ?x
x : Type
Unable to unify "?x" with "x" (cannot instantiate "?x" because "x" is not in
its scope: available 
arguments are "P" "Q" "H").

The proof steps themselves look very phishy already. The proof constructs an existential variables to sit in place of $x$ in the second half, and then tries to instantiate it using the $x$ obtained as premise after applying the hypothesis (forall x, (P x)) -> Q. The proof steps look cyclic proof to me.

What in general does this message imply? What types of logical mistake does this message indicate here?


There is a recent github issue from Coq actually indicates that instantiating evars outside of scope CAN prove falsehood, except that it's blocked by QED.

https://github.com/coq/coq/issues/8215

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top