7
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ You are not going to be able to prove this constructively. You can if you assume some suitable axiom of classical logic. $\endgroup$ – Derek Elkins left SE Sep 22 '17 at 3:35
  • 2
    $\begingroup$ @DerekElkins I learned that. but would the out of scope instantiation reveals the reason why this won't work in constructive logic? $\endgroup$ – Jason Hu Sep 22 '17 at 3:53
  • 1
    $\begingroup$ I wouldn't say so though it does start to suggest it. There all kinds of ways of failing to prove this constructively, and obviously all approaches need to fail for this not to be provable. Constructively proving an existential requires producing a witness. In this case we need to create an arbitrary value of an arbitrary type which is impossible and none of the assumptions provide us with a value of the type. The law of excluded middle, on the other hand, allows us to magic up values out of nowhere. $\endgroup$ – Derek Elkins left SE Sep 22 '17 at 4:30
  • 1
    $\begingroup$ The standard proof of LEM in classical sequent calculus is indeed "a variable escaping its scope". Haven't looked too closely at this one but it could be that you'd have a similar situation. $\endgroup$ – gallais Sep 22 '17 at 12:40
  • $\begingroup$ Did you really mean (P : Type -> Prop)? And not (A : Type) (P : A -> Prop)? If you meant the latter, then you can prove the negation of your lemma. $\endgroup$ – Anton Trunov Sep 22 '17 at 13:22
8
$\begingroup$

When you do an existential introduction, you are saying there is some term $t$, which is represented by the unification variable ?x, such that $P(t)\to Q$. You then try to apply $P(t)$ to $H : (\forall x.P(x)) \to Q$. It tries to generalize P ?x, because if it can show that $P(c)$ for a fresh constant $c$ (represented by x in the Coq output), then $\forall x.P(x)$ would follow. It attempts to unify that fresh constant, x, with the unification variable ?x, but this is disallowed. From a logical perspective, ?x represents a term $t$ and that term is, by definition freshness, distinct from the fresh $c$ (i.e. x) which is just to say $c$ wasn't in scope when we introduced $t$, so $t$ can't have depended on it.

As a simpler scenario, we can't prove $\exists x.\forall y.x = y$ by using existential introduction with $y$. $y$ isn't in scope at that point.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.