Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
  • Date: Wed, 17 Aug 2016 16:16:23 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
  • Ironport-phdr: 9a23:eoImOh8LyRB1Cf9uRHKM819IXTAuvvDOBiVQ1KB92+McTK2v8tzYMVDF4r011RmSDNydsasP27qe8/i5HzdRudDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvjotuJOk4Y1HL9Oeo0d0Tu612J94E/ushLEu4J0BzHo39FKax95FhDAhatpSv6/dq655V58i5d6LoL/s9EVrjmLexjFeQLRGduD2dgrsbsrFzISRaFznoaSGQf1BRSSUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3pZxsRRD0kiAfc3Yc8WrXg8F0xuoPpROqpxVyx8jPZ4yaKOB5Zovce88XQSxKWcMHBH8JOZ+1c4ZaV7lJBu1ftYSo/1Y=

Dear Coq Users,

 

I am stuck with a proof that two proofs of equality are equal:

 

Goal forall (T : Type) (feq : Eq=Eq->T) (H1 : Eq=Eq), feq eq_refl = feq H1.

intros.

 

T : Type

feq : Eq = Eq -> T

H1 : Eq = Eq

______________________________________(1/1)

feq eq_refl = feq H1

 

I know that in general I need proof irrelevance to show that two instances of the same Prop instance are equal, but I wonder if there is some trick to do this for equalities without an axiom.

 

As far as I know “@eq_refl comparison Eq” is the only possible proof of Eq=Eq, so shouldn’t all proofs of Eq=Eq be equal to “@eq_refl comparison Eq” ? Is there a way to prove this?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928




Archive powered by MHonArc 2.6.18.

Top of Page