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?
Chronological Thread
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
- Date: Wed, 17 Aug 2016 19:28:39 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f177.google.com
- Ironport-phdr: 9a23:yHQQUx2KGXJ2swWbsmDT+DRfVm0co7zxezQtwd8ZsegTLfad9pjvdHbS+e9qxAeQG96KsrQe0KGM7uigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV8Tz2DgKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduYCgJ45jgsgCGRg+S7FMdVH8Xm1xGGVvr9hb/C7X2tCLmtuN7kA2XPNP7S6x8DTal6aZoRRvlhQ8IMjc49Cfcjckm3/ETmw6ouxEqm92cW4qSLvcrJq4=
On 08/17/2016 07:24 PM, Jason Gross wrote:
Oooh, nice!
Something strange seems to be going on here, though. Why does this not
replace H1 with eq_refl?
Goal forall (T : Type) (feq : Eq=Eq->T) (H1 : Eq=Eq), feq eq_refl = feq H1.
intros.
revert dependent H1.
refine (fun H1 => match H1 with eq_refl => _ end).
But, this does work (replacing the hole in the refine with eq_refl):
Goal forall (T : Type) (feq : Eq=Eq->T) (H1 : Eq=Eq), feq eq_refl = feq H1.
intros.
revert dependent H1.
refine (fun H1 => match H1 with eq_refl => eq_refl end).
Qed.
That's another strange behavior of return clause inference - sometimes it needs help like this, and sometimes not.
-- Jonathan
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, (continued)
- 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
- 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?, Jean-Marie Madiot, 08/17/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Maxime Dénès, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Hugo Herbelin, 08/18/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?, 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/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Amin Timany, 08/18/2016
- RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Guillaume Melquiond, 08/18/2016
- RE: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Soegtrop, Michael, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Jonathan Leivent, 08/18/2016
- Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, Pierre Courtieu, 08/18/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?, John Wiegley, 08/17/2016
Archive powered by MHonArc 2.6.18.