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

Question

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?

Answer 1

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.

Answer 2

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.