coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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

[Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/17/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, John Wiegley, 08/17/2016
  - Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jason Gross, 08/17/2016
    - Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jonathan Leivent, 08/17/2016
      - Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, ikdc, 08/17/2016
        
        Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jonathan Leivent, 08/17/2016
      - RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/17/2016
        
        Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jason Gross, 08/17/2016
        
        Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jean-Marie Madiot, 08/17/2016
        
        Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Hugo Herbelin, 08/17/2016
        Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jason Gross, 08/18/2016