Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proof uninformativeness vs. proof irrelevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof uninformativeness vs. proof irrelevance


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
  • Date: Sat, 23 Apr 2016 21:00:06 -0400
  • Authentication-results: mail3-smtp-sop.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-f173.google.com
  • Ironport-phdr: 9a23:iQOBSxz1JJf8cuPXCy+O+j09IxM/srCxBDY+r6Qd0e4XIJqq85mqBkHD//Il1AaPBtWLra0ewLCO6OjJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6CyZvtnLrqoNX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6t4X0VTmUflFJsDgnb4RfmFsPztS37ted51SSyMsj/TLRyUjOnufQ4ACT0gTsKYmZquFrcjdZ92fpW



On 04/23/2016 08:41 PM, darktenaibre wrote:
Ah, that notprop predicate prevents this stupid observation though. You can certainly write something like (fun T => forall P : Prop, ~ (@eq Type P T)) which will easily block the previous proof, but it's probably unusable this way. I do not have any idea for a clever solution to this problem though.
On 04/24/2016 02:32 AM, darktenaibre wrote:
On 04/24/2016 02:21 AM, Jonathan Leivent wrote:

Definition proof_uninformativeness := forall (P : Prop)(S : Set)(f : P -> S)(p1 p2 : P), f p1 = f p2.
Hi,
If you take f:=id, isn't it just proof irrelevance ?


Lemma proof_uninformativeness_irrelevance : proof_uninformativeness -> forall (P : Prop) (p q : P), p = q.
intros pu P; apply pu.
Qed.

Oops - my (embarrassing) mistake having Prop not be a subtype of Set. :-[

So, there would need to be some usable notprop predicate.
Hmm... maybe types having at least 2 distinguished instances are sufficient? :

Definition distinguished(T : Type) := exists (a b : T), a <> b.

Definition proof_uninformativeness := forall (P : Prop)(T : Type)(f : P -> T)(p1 p2 : P), distinguished T -> f p1 = f p2.

Is this a suitable replacement for all interesting use cases of proof irrelevance?

-- Jonathan





Archive powered by MHonArc 2.6.18.

Top of Page