Как доказать (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

Вы можете использовать tauto, чтобы доказать это автоматически:

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), один для доказательства цели (P), используя левый вывод (P) of or, и один, чтобы доказать цель (P), используя правильный вывод (Q).

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.