coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] LEM variants vs. proof relevance
- Date: Sun, 29 May 2016 02:26:37 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f42.google.com
- Ironport-phdr: 9a23:AtoezRJUhPe5XAi91NmcpTZWNBhigK39O0sv0rFitYgUKfTxwZ3uMQTl6Ol3ixeRBMOAu6MC1rKd6fm/EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxirj5ocSMKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1kVSWIQ2jVSBBPepEX4V4z2tCTgsfFmiQGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=
Have you considered LEM on hProps?
forall P, (forall x y : P, x = y) -> P \/ ~P
Together with propositional truncation / quotient types, this may give you want you want. (I think these are similar to your irrelevant_sibling; you do:
Module Export Trunc.
Private Inductive PropTrunc A := tr : A -> PropTrunc A.
Axiom PropTrunc_trunc : forall {A} (x y : PropTrunc A), x = y.
Definition Trunc_ind {A}
(P : PropTrunc A -> Type) {Pt : forall x y, P x = P y}
: (forall a, P (tr a)) -> (forall aa, P aa)
:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
End Trunc.
)
Does this do what you want?
On Sat, May 28, 2016 at 5:14 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:
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.