How to prove the lemma "(P \ / Q) / \ ~ P & # 8594; Q." in coq?

Question

I tried to prove this lemma with tatami [intros], [apply], [assumption], [destruct], [left], [right], [split], but it did not work. Can someone teach me how to prove this?

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

And anyway, how to prove simple sentences like false-> P, P / ~ P, etc.

Answer 1

A tactic that you are missing is a contradiction that is used to prove goals that contain conflicting hypotheses. Since you are not allowed to use the contradiction, I believe that the lemma you are going to apply is the induction principle for False. After that, you can apply the negative sentence and close the branch by assumption. Please note that you can do better than your instructor and not use any of these tactics! The proof for disjunctive syllogism is relatively easy to write:

 Definition dis_syllogism (PQ : 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 PQ : Prop. Lemma a : (P \/ Q) /\ ~P -> Q. intros. inversion H. destruct H0. contradiction. assumption. Qed. End Example. 

Answer 3

To prove all these simple things, you have a family of tauto , rtauto , intuition and firstorder .

I believe that they are stronger than the taut, which is the complete procedure for adopting the intuitionistic logic of utterances.

Then intuition allows you to use some hints and lemmas to use, and firstorder can talk about first-order inductance.

More details in the doc , of course, but this is the kind of tactic you want to use to achieve such goals.

Answer 4

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

 Lemma a : forall (PQ: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.