coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof irrelevance for Z.le

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: Thomas Braibant <thomas.braibant AT gmail.com>
Cc: Daniel Schepler <dschepler AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof irrelevance for Z.le
Date: Wed, 01 Aug 2012 02:26:03 +0200

On 31/07/2012 21:24, Thomas Braibant wrote:

Actually, I think that Z.le could be defined as
Definition Zle n m := n ?=m = Lt \/ n ?= m = Eq.

This definition is compatible with proof irrelevance, and should be
completely equivalent with the previous one. I may try to submit a
feature request about that one, but I wonder if it is worth it.

Usually, the good way to go when you want to have proof irrelevance on a decidable property is to replace every "P x" with "P_dec x = true". This is generic and easy to handle, so I don't really see the need to change any definition in particular...

PMP

Re: [Coq-Club] Proof irrelevance for Z.le, Pierre-Marie Pédrot, 08/01/2012