Search code examples
logiccoq

How to prove in Coq ~~(P \/ ~P)

I want to prove ~~(P \/ ~P) in Coq, which sounds somehow trivial... However I do not know where to go since there is not any single hypothesis. I have written the following code which is not working, since it is giving the following exception [ltac_use_default] expected after [tactic] (in [tactic_command]).

Parameter P: Prop.

Section r20.
Lemma regra1: ~~(P \/ ~P).
Proof.
  intro.
   - cut P.
   - cut ~P
Qed.
End r20.
Solution

  • It is little tricky one. Here is one way to prove it.

    Parameter P : Prop.

Section r20.
Lemma regra1: ~~(P \/ ~P).
Proof.
  unfold not. intros H1.
  apply H1. right.
  intros H2.
  apply H1. left.
  exact H2.
Qed.
End r20.