CODEWITHSUNDEEP
logiccoq
Breno
Breno

Reputation: 165

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.

Upvotes: 0

Views: 421

Answers (1)

Divyanshu Ranjan
Divyanshu Ranjan

Reputation: 1625

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.

Upvotes: 0

Related Questions