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: Jean-Marie Madiot <jmadiot AT CS.Princeton.EDU>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
- Date: Wed, 17 Aug 2016 16:10:17 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jmadiot AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=jmadiot AT cs.princeton.edu; spf=None smtp.helo=postmaster AT greenlight.cs.princeton.edu
- Ironport-phdr: 9a23:p2HAFhJ9Wzaraa4yUNmcpTZWNBhigK39O0sv0rFitYgUI/rxwZ3uMQTl6Ol3ixeRBMOAuqsC0bCd6/6oGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMS3nHlP/sydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1e0h83sDgtAHCQA2T/TNcFzxOylsbSzTCuTr9R9/atjbw/r523zDfNsnrR5g1Xy6j5uFlUkm7pj0AMmsb/WjRz+l5lqNW6Deoqx1438aAYoScOPt5Yov2RpUiX2tHVctNUCoHL6+BOdhcR9EdNPpV+tGu72AFqgGzUEz1XLvi
More precisely (my guess is) that it works when "being equal to the given *element* of the type" is decidable (or more simply, can be done with a finite pattern matching term).
For exemple, equality on streams is not decidable, but we can decide equality to a finite stream. And the same refine tactic works. However, try it with an infinite stream, and it fails to help.
CoInductive stream :=
| nil : stream
| cons : nat -> stream -> stream.
Lemma test1 :
forall (T : Type)
(feq : cons 3 nil = cons 3 nil -> T)
(H1 : cons 3 nil = cons 3 nil),
feq eq_refl = feq H1.
Proof.
intros T feq H.
refine (match H with eq_refl _ => _ end).
reflexivity.
Qed.
Lemma test2 :
forall (T : Type)
(feq : (cofix x := cons 3 x) = (cofix x := cons 3 x) -> T)
(H1 : (cofix x := cons 3 x) = (cofix x := cons 3 x)),
feq eq_refl = feq H1.
Proof.
intros T feq H.
Fail progress refine (match H with eq_refl _ => _ end).
Abort.
On Wed, Aug 17, 2016 at 3:55 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
It only works if the type has decidable equality. list nat has decidable equality. It is also decidable whether or not a list of any type is nil, or not. If you instead try (feq : Set::nil = Set::nil -> T), you will find that it does not work. If you try (feq : Set = Set -> T) it will not work. If you try (feq : list nat = list nat -> T), it will not work. If you try (feq : S = S -> T) it will not work. If you try (feq : eq_refl 0 = eq_refl 0 -> T), it may or may not work (this still has decidable equality, but it is more complicated).On Wed, Aug 17, 2016 at 12:04 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:Dear Jason, Jonathan,
thanks for the solution and explanation.
I experimented a bit. I think that this works for any literal term of any type, even if it doesn't have decidable equality. E.g.:
Open Scope list_scope.
Lemma TestNatList: forall (T : Type) (feq : 3::nil=3::nil->T) (H1 : 3::nil=3::nil), feq eq_refl = feq H1.
Proof.
intros.
refine (match H1 with
| eq_refl _ => _
end).
reflexivity.
Qed.
The resulting proof term is lengthy. I guess the decidable equality is required if the value compared is not a literal, but a parameter.
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
- 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?, 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.