coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] About the meaning of proof-irrelevance

From: "Gyesik Lee" <leegys AT gmail.com>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] About the meaning of proof-irrelevance
Date: Thu, 20 Nov 2008 10:39:57 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type :content-transfer-encoding:content-disposition; b=tS9/FqBg+KjYigBdhnLCiu9DJJADwvLcpF1t2Z4OBKgnLvx1pdRazfDVGN979iYTGw ZR5Mr8Hu+a3WPQ5EWOBlpyGfGymT8l6B+zSMQBpD0TEFT853J+VU9LlHGJyfkwL5bcI/ 8iDQQfQUC3SQKo0mR8QEk/Sw/uXlfl0P62TSg=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear coq-users,

some time ago there was a discusstion about how to prove the proof-irrelevance
of "less than" relation,
that is,

forall (m n:nat) (P Q: m <= n), P = Q.

It was really interesting to see the proof.
However, I found it a bit strange because there are obviously more
than one proof for (m <= n).
(You can e.g. apply the cut rule arbitrarily many times using 0 = 0 ->
0 = 0 -> ... -> m <= n.)

Then I noticed that they are equal modulo beta-and/or eta-congruence.

Are there more things assumed in the background?

[Coq-Club] About the meaning of proof-irrelevance, Gyesik Lee
- Re: [Coq-Club] About the meaning of proof-irrelevance, Arnaud Spiwack