patternMinor
What does instantiating existential variables with out of scope variable imply?
Viewed 0 times
implyinstantiatingwhatwithscopedoesvariablesexistentialvariableout
Problem
I have following unfinished proof of a lemma:
The problem is the last
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
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
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 messageError:
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
Solution
When you do an existential introduction, you are saying there is some term $t$, which is represented by the unification variable
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.
?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.
Context
StackExchange Computer Science Q#81510, answer score: 9
Revisions (0)
No revisions yet.