coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?
Date: Thu, 03 Sep 2015 11:03:53 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.casteran AT labri.fr; spf=Pass smtp.mailfrom=pierre.casteran AT labri.fr; spf=Pass smtp.helo=postmaster AT iona.labri.fr
Ironport-phdr: 9a23:efqu2xNOl88jD1UmReMl6mtUPXoX/o7sNwtQ0KIMzox0KPj4rarrMEGX3/hxlliBBdydsKIYzbKK+PiwEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35jxj7z5o82bSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7a3noRSH8b2jFBGBTI9hj8FsPpsybgrOc70yCBIcDsRLYcXT2o9aYtRgW+23RPDCIw7GyC0p84t6lcuh/0/xE=
Organization: LaBRI - Université Bordeaux 1 - France

Hi,

Assuming ~(A \/ ~A), you first prove ~A, then find a contradiction.

Goal forall A:Prop, ~ ~(A \/ ~A).
intros A H.
apply H.
right;intro a.
destruct H;now left.
Qed.

Pierre

Le 03/09/2015 10:54, shengyu shen a écrit :

Dear all:

I am trying to prove an exercise in coq art “∀A: Prop, ∼∼(A∨∼A).”

I think this may need exclude middle rule, which is not in “Calculus of
Inductive Constructions“

am I right?

Shen

[Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, shengyu shen, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Pierre Casteran, 09/03/2015
  - Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Arnaud Spiwack, 09/03/2015
    - Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, shengyu shen, 09/03/2015
- Re: [Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?, Dominique Larchey-Wendling, 09/03/2015