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 16:33:54 -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-qk0-f172.google.com
  • Ironport-phdr: 9a23:5kKYJhY8Hz+aCeEnlY8OQGT/LSx+4OfEezUN459isYplN5qZpci7bnLW6fgltlLVR4KTs6sC0LqH9f24EjVcvt6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDjvcCLKFwU23KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA0lRxBHwjM6lneU5bvvy3m/r5/3y+bPsDyQL0cVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy
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