coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 |
- [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Gérard Huet, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Arnaud Spiwack, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/30/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/30/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Arnaud Spiwack, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Gérard Huet, 05/28/2016
Archive powered by MHonArc 2.6.18.