Skip to Content.
Sympa Menu

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

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




Archive powered by MHonArc 2.6.18.

Top of Page