coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Gyesik Lee" <gyesik.lee AT aist.go.jp>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] About the meaning of proof-irrelevance proof
Date: Wed, 19 Nov 2008 20:47:29 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:mime-version:content-type :content-transfer-encoding:content-disposition:x-google-sender-auth; b=vNjpnmWbj5dQyhEAgJ6i4Z4wJ3j+U4y6n3jX/hNwNfXKRFzwq/PjDBYFTJZIUkEnEc 8j83k4BY7zsY83w0jE7CLXGseXv3Fi8sHNSSX2KWPwmN6MmYC4vIvKRchA2ICi0mYUzs 9UE0wzqYqrz7TQSBUiee3HO0Twea1K4FtI/F4=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear coq-users,

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

forall (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.
(You can e.g. apply the cut rule arbitrarily many times.)
Then I noticed that everything is proved modulo beta-and/or eta-congruence.

My question is, is it so?
Or are there more things assumed than beta-, eta-congruence?

[Coq-Club] About the meaning of proof-irrelevance proof, Gyesik Lee