The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Okay, it seems that I thought about Prop-s on decidable (is it correct to say? maybe constructable?) sets.

So the correct question is about the proof irrelevance of such proofs. For example, a = b, a<>b, a<b, a*a<b on nat etc., or maybe some example on list nat (proof irrelevance for Prop "is a list sorted", for example) or others.

On Wed, Oct 23, 2013 at 2:37 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

No.  For example, the type

Inductive bool_in_prop : Prop := trueP | falseP.

does not have provable irrelevance.  (You can neither proof [trueP = falseP] nor [trueP <> falseP].)  It is clearly decidable, though, because [left trueP : {bool_in_prop} + {~bool_in_prop}].

I'm not sure if there's a general way to make such proofs, but I suspect there might be, at least for inductively defined [Prop]s.

For your specific case, I think you might need to assume functional extensionality (and then prove trivially that all inhabitants of [False] are equal).  Otherwise, I think there is no way to prove a non-trivial function equality, though I may be wrong.

-Jason

On Tuesday, October 22, 2013, Ilmārs Cīrulis wrote:

Is it true that for all decidable Prop there is provable proof irrelevance?

If it's true, is there any general way how to make such proofs?

Also more specifically - how I can prove that
forall (n m:nat) (p1 p2: n<>m), p1 = p2 ?