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: 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



    




Archive powered by MHonArc 2.6.18.

Top of Page