Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] LEM variants vs. proof relevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] LEM variants vs. proof relevance


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] LEM variants vs. proof relevance
  • Date: Sat, 28 May 2016 17:14:29 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f48.google.com
  • Ironport-phdr: 9a23:JllquheDZvvN3c3H11K6ZrxplGMj4u6mDksu8pMizoh2WeGdxc6+ZR7h7PlgxGXEQZ/co6odzbGG4ua9ASdZvM7JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuOO04R2WL1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDsB1OChTF5ReyeprwrCb8qqIp2i6cPM77Sb05cTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==



On 05/28/2016 04:56 PM, Arnaud Spiwack wrote:
Hum:

Variable P:Prop.

Goal (P \/ (P \/ ~P -> ~P)) <-> (P \/ ~P).
Proof.
  tauto.
Qed.

Exercise: why is it clear?

Remark: tauto is complete on propositional logic.

Oops ...  Hmm...  Looks like at one point I had "P \/ (P \/ ~P -> P)" instead - but that doesn't work.  OK - driver error. :-[

Does the irrelevant_sibling thing seem more promising?  That seems like as weak as it can be and still do the job.

-- Jonathan

​

On 28 May 2016 at 22:33, Jonathan Leivent <jonikelee AT gmail.com> wrote:

After some more thought - maybe the simple and direct route is better -
which works even without proof relevance:

Axiom irrelevant_sibling : forall P, {Q | (Q <-> P) /\ (forall a b : Q, a
= b)}.

Definition piP (p : Prop) : Prop.
Proof.
  destruct (irrelevant_sibling p) as (q & i & e). exact q.
Defined.

Lemma piP_iff_P : forall P, piP P <-> P.
Proof.
  unfold piP. intro p.
  destruct (irrelevant_sibling p) as (q & i & e). exact i.
Qed.

Lemma piP_irrelevant : forall P (a b : piP P), a = b.
Proof.
  unfold piP. intro p.
  destruct (irrelevant_sibling p) as (q & i & e). exact e.
Qed.

It's still required that irrelevant_sibling not imply proof
irrelevance...  It certainly *looks* weaker...

-- Jonathan



    
    



Archive powered by MHonArc 2.6.18.

Top of Page