Assume Half a Disjunctive Premise for "or elimination" Proof

2
votes

I think by this point I've read most if not all of the 81 questions tagged . Being very new to coq, I was unable to find an answer to this very simple question (which I'm fairly certain has not been asked on SO because of how basic it is).

I am working on a homework assignment, for which I need to use coq to prove:

  • Given: P/Q. ~Q
  • Prove: P

This is a simple enough proof for me to do on paper, but I can't seem to get coq to do this for me.

My strategy is to assume each of P and Q, to show P and therefore conclude that P must hold:

  1. P / Q [Premise]

  2. ~Q [Premise]

    1. P [Assumption]

    2. P [Copy Previous Line]

    3. Q [Assumption]

    4. ~Q [Copy Previous Line]
    5. [Contradiction]
    6. P [Contradiction Elimination]
  3. P [Elimination of \/]

Given that this is how I would prove it on paper, I was able to come up with the following coq code to prove it in coq. Sadly my effort to assume P, Q, or ~P don't come through:

Section Q5.

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

Goal P.

Here are my attempts for the next line, along with the errors they produce:

+-----------------+---------------------------------------------------------------------+
|      Code       |                                Error                                |
+-----------------+---------------------------------------------------------------------+
| assumption.     | Error: No such assumption.                                          |
| exact P.        | The term "P" has type "Prop" while it is expected to have type "P". |
| apply premise1. | Error: Impossible to unify "P \/ Q" with "P".                       |
| apply P.        | Error: Impossible to unify "Prop" with "P".                         |
+-----------------+---------------------------------------------------------------------+

I'd appreciate any help with this since I've exhausted everything that I can think of at this point.

1
coq

1 Answers

3
votes

I'm not sure I understand your strategy well, but it seems right.

What you want to do is basically consider the two cases of the P \/ Q disjunction. This can be done via the tactic destruct premise1., which will yield two goals, one in which p: P, and one in which q: Q. These two should be easy to prove.

For the reasons why your tactics failed:

P : Prop
Q : Prop
premise1 : P \/ Q
premise2 : ~ Q
______________________________________(1/1)
P

  1. assumption. will not work because it just looks in your hypotheses for a term whose type is your current goal. There is no term at type P here.

  2. exact P. will fail because the tactic exact <term>. is supposed to solve a goal <type> if <term> : <type>. Your goal is not Prop, right? :)

  3. apply premise1. will fail because it only applies on a goal P \/ Q.

  4. apply P. is basically the same as exact P. at that point.

Overall, you seem to have a (common) problem thinking apart terms and types. Remember that your goal is a type, which you try to prove by building a term. Your hypotheses are all of the form <term> : <type>, so whenever you use exact <term>. or apply <term>., it's because the stuff on the right of the colon after <term> matches your goal, not the name on the left of the colon.