How to prove the lemma "(P \/ Q) /\ ~P -> Q." in coq?

5
votes

I tried to prove this lemma with the tatics [intros], [apply], [assumption], [destruct],[left], [right], [split] but failed. Can anyone teach me how to prove it?

Lemma a : (P \/ Q) /\ ~P -> Q.
proof.


And generally, how to prove the easy propositions such as false->P, P/~P, etc?

4
coq
See also How to do cases with an inductive type in Coq, which discusses a different but related lemma – Gilles 'SO- stop being evil'
@cachuanghu please note that although it is not necessary, it is customary, and you'll get a couple of reputation points, if you mark an answer that is good enough for you as "accepted". Your comment indicates that you found your way through your difficulty. If none of the answers here contained your way, you may feel free to write your own answer and mark it as "accepted". An accepted answer will be helpful to people like me who are still learning some of these Coq tactics. – minopret
Sorry for that. I have voted for the accepted answer. And is there any thing else should i do? – cachuanghu

4 Answers

5
votes

The tactic that you are missing is contradiction, which is used in order to prove goals containing contradictory hypotheses. Because you aren't permitted to use contradiction, I believe the lemma you are intended to apply is the induction principle for False. After doing so, you can apply the negated proposition and close the branch by assumption. Note that you can do better than your instructor requested, and use none of the listed tactics! The proof term for disjunctive syllogism is relatively easy to write:

Definition dis_syllogism (P Q : Prop) (H : (P ∨ Q) ∧ ¬P) : Q :=
  match H with
    | conj H₁ H₂ =>
      match H₁ with
      | or_introl H₃ => False_ind Q (H₂ H₃)
      | or_intror H₃ => H₃
      end
  end.
3
votes
Section Example.

  (* Introduce some hypotheses.. *)
  Hypothesis P Q : Prop.

  Lemma a : (P \/ Q) /\ ~P -> Q.
    intros.
    inversion H.
    destruct H0.
      contradiction.
      assumption.
  Qed.

End Example.
2
votes

To prove all these easy things, you have the family of tactics tauto, rtauto, intuition and firstorder.

I believe they are all stronger than tauto, which is a complete decision procedure for intuitionistic propositional logic.

Then, intuition allows you to put in some hints and lemmas to use, and firstorder can reason about first-order inductives.

More details in the doc of course, but these are the kind of tactics you want to use on such goals.

0
votes

Remember that ~P means P->False, and inverting a False hypothesis finishes the goal (since False has no constructors). So you really just need apply and inversion.

Lemma a : forall (P Q:Prop), (P \/ Q) /\ ~P -> Q.
Proof.
  intros. 
  inversion H.
  inversion H0.
  - apply H1 in H2.  (* applying ~P on P gives H2: False *)
    inversion H2.
  - apply H2.
Qed.