coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2)

From: Benoît Viguier <beviguier AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2)
Date: Thu, 25 Feb 2016 18:14:15 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f47.google.com
Ironport-phdr: 9a23:3BJZaRW6M4Ki4ONx9DWQjMnjl/DV8LGtZVwlr6E/grcLSJyIuqrYZheAt8tkgFKBZ4jH8fUM07OQ6PC/HzJZqsvR+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVPVwD2Wr1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDuBdOBI7Z2y/7UYrwvzGy4uBwxiiVIMz7V5g7XD2j6+FgTxq+23RPDCIw7GyC0p84t6lcuh/0/xE=

Hi,

I'm also on the learning curve of Coq. My guess is that you are missing :

Lemma NNPP : forall p:Prop, ~ ~ p -> p.

when you do not have Classical wich is why auto fails.

Require Import Coq.Setoids.Setoid.

Theorem test : forall (P1 P2 : Prop),
(P1 <-> ~ P2) <-> (~ P1 <-> P2).
Proof.
intros.
intros P1 P2.
split ; intro Eq.
split.
intros NP1.
rewrite Eq in NP1.

And then you can't go on. :/

Benoît.

2016-02-25 17:52 GMT+01:00 Stefan Ciobaca <stefan.ciobaca AT gmail.com>:

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