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: darktenaibre <darktenaibre AT isomorphis.me>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
  • Date: Sun, 24 Apr 2016 02:32:31 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=darktenaibre AT isomorphis.me; spf=Pass smtp.mailfrom=darktenaibre AT isomorphis.me; spf=None smtp.helo=postmaster AT macaron.isomorphis.me
  • Ironport-phdr: 9a23:PY0Z+x9pEFdCB/9uRHKM819IXTAuvvDOBiVQ1KB91+4cTK2v8tzYMVDF4r011RmSDdWdtKgP0ruK+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt6U0J78jrHus7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGAeG/HgAX2MfkxBSDkCR4BjgXYv8tCL7vPBw8CiBOsjxV6g0WC/k6qo9G0ygszsOKzNsqDKfscd3lq8O+B8=
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.

Archive powered by MHonArc 2.6.18.

Top of Page