如何證明（R - > P）[Coq證明助理]？

Question

如何證明（R-> P）在Coq中。我是這方面的初學者，並且不太瞭解這個工具。這是我寫的：

Require Import Classical. 

Theorem intro_neg : forall P Q : Prop,(P -> Q /\ ~Q) -> ~P. 
Proof. 
intros P Q H. 
intro HP. 
apply H in HP. 
inversion HP. 
apply H1. 
assumption. 
Qed. 

Section Question1. 
Variables P Q R: Prop. 
Hypotheses H1 : R -> P \/ Q. 
Hypotheses H2 : R -> ~Q. 
Theorem trans : R -> P. 
Proof. 
intro HR. 
apply NNPP. 
apply intro_neg with (Q := Q). 
intro HNP. 

我只能說到這一點。

在這一點上，子目標是：

1 subgoals 
P : Prop 
Q : Prop 
R : Prop 
H1 : R -> P \/ Q 
H2 : R -> ~ Q 
HR : R 
HNP : ~ P 
______________________________________(1/1) 
Q /\ ~ Q 

Answer 1

您可以使用同田自動證明這一點：

Section Question1. 
Variables P Q R: Prop. 
Hypotheses H1 : R -> P \/ Q. 
Hypotheses H2 : R -> ~Q. 
Theorem trans : R -> P. 
Proof. 
intro HR. 
tauto. 
Qed. 

如果你想手動證明這一點，H1說，鑑於R，是p或者Q是真的。所以如果你破壞H1，你會得到3個目標。一個用來證明前提（R），一個用or的左邊結論（P）來證明目標（P），另一個用正確結論（Q）來證明目標（P）。

Theorem trans' : R -> P. 
Proof. 
intro HR. 
destruct H1. 
- (* Prove the premise, R *) 
    assumption. 
- (* Prove that P is true given that P is true *) 
    assumption. 
- (* Prove that P is true given that Q is false *) 
    contradiction H2. 
Qed. 
End Question1.