coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Stefan Ciobaca <stefan.ciobaca AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2)
Date: Thu, 25 Feb 2016 18:52:33 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stefan.ciobaca AT gmail.com; spf=Pass smtp.mailfrom=stefan.ciobaca AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f169.google.com
Ironport-phdr: 9a23:WniqhxyHDWi5BHvXCy+O+j09IxM/srCxBDY+r6Qd0e4UIJqq85mqBkHD//Il1AaPBtWErawdwLeM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU0Z38irr60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWdheC6HIaGk4XlRBBCAGNuArmU5n4tG3xt+130SKTFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==

Hello, coq-club!

I'm wondering if the following is provable constructively:

forall (P1 P2 : Prop),

(P1 <-> ~ P2) <-> (~ P1 <-> P2).

The tactic tauto solves it in the presence of EM:

Require Import Classical.

Lemma P1_if_not_P2 :

forall (P1 P2 : Prop),

(P1 <-> ~ P2) <-> (~ P1 <-> P2).

Proof.

intros.

tauto.

Qed.

But tauto fails without the Classical module.

Best wishes,

Stefan Ciobaca

[Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Stefan Ciobaca, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Benoît Viguier, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Jonathan Leivent, 02/25/2016
  - Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Julian Michael, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Robbert Krebbers, 02/25/2016
  - Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Julian Michael, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Ralf Jung, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Michel Levy, 02/25/2016