모순에 의한 증명에 대한 부정적인 가정

Question

나는 많은 규칙을 가지고 있는데, 그것은 근본적으로 어떤 명제 P가 결코 사실 일 수 없다는 것을 의미한다. 이제 Coq를 사용하여 P가 거짓임을 증명해야합니다. 종이에 그렇게하기 위해서, 나는 P가 붙잡고 모순에 빠져 있다고 가정하고, P는 유지할 수 없다는 것을 증명합니다.

P가이 증명을 위해 보유하고 있다고 가정하는 방법에 대해 확신 할 수 없습니다. 이는 내가 도움을 구하는 것입니다. 내 현재 코드 : 나는 이것에 대해 올바른 방법 (? 또, 어떻게이 일을해야한다)을거야 여부를

Variables {…} : Prop. 
Hypothesis rule1 : … . 
Hypothesis rule2 : … . 
. 
. 
. 
Hypothesis rule6 : … . 
Variable s : P. (* Assume that P holds for proof by contradiction *) 
(* other Coq commands *) 
(* proof is done *) 

사람이 확인시겠습니까?

Theorem notP := P -> False. 

그래서, 형 P의 변수와 함께, 당신은 거짓 목표를 증명해야합니다

Theorem notP := ~ P. 

로 귀결되는 : 당신이 원하는 무엇

Answer 1

증명하는 것입니다.

나는 당신이 그것을하고있는 방식은 받아 들일 만하다고 생각한다. 아마 당신이 원하지 않을 다른 곳에서 그걸 도달 할 수 없도록 섹션에 Variable s : p.을 넣고 싶을 것이다.

Section ProvingNotP. 
Variable p : P. 
Theorem notP: False. 
Proof. ... Qed. 
End ProvingNotP. 

나는 이것이 효과가 있다고 생각한다.