coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "John Wiegley" <johnw AT newartisans.com>
To: "Soegtrop\, Michael" <michael.soegtrop AT intel.com>
Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
Date: Wed, 17 Aug 2016 09:23:03 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f50.google.com
Ironport-phdr: 9a23:QClGlR1DESbNS7CMsmDT+DRfVm0co7zxezQtwd8ZsekXK/ad9pjvdHbS+e9qxAeQG96KsrQe0qGG4+igATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV8Rz2rtKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduGykP6cbqrRjOSxeUrjtZCz1O00kAPw+Qpir9U5jtqCzigq41/SiRPcT7Sfp8DTGj5KdiRRuukyAKOCIj93n/i8psgaYdqxWk8U9R2YnRNcu3M/p4NpzccNweSHsLFpJTUCxHHau6YpQGFfYAJu9etM/2oF5Y/kj2PhWlGO66kmwAvXTxx6Bvlr15SQw=
Organization: New Artisans LLC

>>>>> "SM" == Soegtrop, Michael
>>>>> <michael.soegtrop AT intel.com>
>>>>> writes:

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

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

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

Goal forall (T : Type) (feq : Eq=Eq->T) (H1 : Eq=Eq), feq eq_refl = feq H1.
Proof.
intros.
refine (match H1 with
| eq_refl _ => _ |
end).
reflexivity.
Qed.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[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
        Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jonathan Leivent, 08/18/2016