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: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
Date: Thu, 18 Aug 2016 06:55:27 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f172.google.com
Ironport-phdr: 9a23:EBUbuBV7kFOQSDssGHcwMHqm8abV8LGtZVwlr6E/grcLSJyIuqrYZhGDt8tkgFKBZ4jH8fUM07OQ6PG5HzZbqsjf+DBaKdoXBkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2asc272qiI9oHJZE0Q3XzmMOo0dk7981uZ9pFPx9AzcuBpklqBi0ALUtwe/XlvK1OXkkS0zeaL17knzR5tvek8/dVLS6TwcvdwZ7VZCDM7LzJ9v5Wz5lGQBTeIs3AbSyAdlgdCKwnD9hDzGJnr4QXgse8o+iCBOsu+YqozQi/qu6ViUxjuhz0ALCVo2G7Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZCSA==

Here is another thing that works:
refine (let pf := _ in fun H1 => match H1 with eq_refl => pf end)

On Wed, Aug 17, 2016, 4:28 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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)