Suppose the negation for the proof is contradictory

Question

I have a bunch of rules that essentially suggest that some P sentence can never be true. Now I have to prove that P is wrong using Coq. To do this on paper, I would suggest that P holds, and then comes to a contradiction, thereby proving that P cannot hold on.

I'm not quite sure how to suggest that P is for this proof, and this is what I am turning to for help. My current code is:

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 *) 

Can someone please confirm if I do it correctly (otherwise, how should I do it?)?

Answer 1

What you want to do is prove:

 Theorem notP := ~ P. 

which comes down to:

 Theorem notP := P -> False. 

So, with a variable of type P you need to prove the target False.

I believe the way you do this is valid, although you probably want to put this Variable s : p. to the section so that you can never get to this in other places where you do not want to ...

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

I think this should work.