coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] UIP and decidable equality

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] UIP and decidable equality
Date: Fri, 9 Sep 2016 09:26:49 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga07.intel.com
Ironport-phdr: 9a23:ERomzBWA5yHJrKmZoelk7aDD4QfV8LGtZVwlr6E/grcLSJyIuqrYZhSBt8tkgFKBZ4jH8fUM07OQ6PG5HzJcqs/d+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MiZaAJRwTG5fLlaLROsrAyXuNNcyd9pLb90wR/UqFNJff5XzCVmPwTAsQz745L6x5lu/DhKvOplv+tBWqXzcqByBehdDT8mOm0xotbsuBbfVwyXznoaTmgS1BFPBl6Wv1nBQp7tv36i5aJG0y6AMJiuQA==

Dear Alan,

since I have quite some issues with proof irrelevance of equalities, I find
this quite interesting.

One thing I don't understand: Is "nu_canon" supposed to hold for all "nu" or
just for some specific "nu"? Declaring "nu" as Variable makes me believe the
first, but in eqdec_canon you use a specific nu (nudec), so it is not clear
to me in how far the conclusion of eqdec_canon is equivalent to nu_canon.

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] UIP and decidable equality, Alan Schmitt, 09/09/2016
- Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
    - Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/12/2016
      - Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/12/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/12/2016
        
        Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/13/2016
      - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/13/2016
- RE: [Coq-Club] UIP and decidable equality, Soegtrop, Michael, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
- Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
    - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
      - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
        
        Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/12/2016