8
$\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

Improve this question
$\endgroup$
6
  • 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
    Commented Sep 22, 2017 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
    Commented Sep 22, 2017 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
    Commented Sep 22, 2017 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
    Commented Sep 22, 2017 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
    Commented Sep 22, 2017 at 13:22

1 Answer 1

Reset to default
9
$\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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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