the reference was not found in the current environment

Question

Disclaimer: this is for a homework assignment

I'm a coq noob, so I hope this is not a repeat question. I /have/ looked at this question, but my question seems to be unanswered still.

I have the following premises:

P \/ Q
~Q

I need to prove:

P

My coq code so far:

Section Q5.

Variables Q : Prop.
Goal P.
Hypothesis premise1 : P \/ Q.
Hypothesis premise2 : ~Q.

I get the following error when I try to execute the line Goal P.:

Error: The reference P was not found in the current environment.

These are the solutions that I was able to come up with:

1. Replace Variables Q : Prop. with Variables P Q : Prop.. The problem with this is that P will be assumed as a premise, which it is not
2. Add Variables P. before the goal declaration. This results in a syntax error.

Am I missing something? I don't seem to be able to figure this out.

Answer 1

The proper solution is 1, and the problem you are expecting is wrong.

When you write:

Variable P: Prop.

You are not assuming that P is inhabited (or, that "P holds"), but only that there exists a proposition named P, a "statement" whose validity is not considered here.

This is very different from writing:

Variable p: P.

Which assumes that there is a proof "p" that the type "P" is inhabited (if P has type Prop, p is a proof of the proposition P), and thus assumes that P is true.

---

Also, the reason why:

Variables P.

results in a syntax error is that you need to provide a type for each variable introduced (Coq can't figure it out magically when there is no information leading the type inference engine).

---

So it is perfectly fine to begin your script as:

Section Q5.
Variables P Q : Prop.
Hypothesis premise1 : P \/ Q.
Hypothesis premise2 : ~Q.
Goal P.