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:
- Replace
Variables Q : Prop.
withVariables P Q : Prop.
. The problem with this is thatP
will be assumed as a premise, which it is not - 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.