coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions
Date: Sat, 5 Jun 2021 22:11:47 -0400
Authentication-results: mail3-smtp-sop.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-il1-f178.google.com
Ironport-hdrordr: A9a23:bxPceKCLTTIujFLlHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqynApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPGRbH5SWyuecMbG3t6nHCcCDfeod/A==
Ironport-phdr: A9a23:Oio1axff/+48C/xB3nFPHQ40lGM+RN7LVj580XLHo4xHfqnrxZn+JkuXvawr0AaYG96DsLkd1bCempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgFFiCCzbL9uIhi6ohjdu8gIjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/jKxZrxyhqRJxwJPabp+JO/dlZKzRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt43zqEEVrRu5AwmnGeLhyiVPhn/txq0xzuMsEQPc0ww7GNIOtnvUrM/yNKcJSuC4yLLFzTrGb/xM2Df97JLEfQwmofGJRL99d9faxkYzGQ3flFqQtZDlMC2P1uQLq2WX8eVtWO2vhWMkqw99viaiy8cth4XVmo4Z1l7J+CZkzIs0ONG1RkF2bNynHZZTsyyWK4R4T90+T2xrpSs0xKELtJimdyYEz5QnwgTQa/2Bc4WQ4xLjUvyRITZii35/drK/nRC/+lWjxO3kTsS4zkpGoy5fntTPtn0BzQHf58mGR/dn40us2zWC2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmErsja+Wclwo+ums6+j6e7nmqIKQOo13hw3kPaQuncu/Aes8MgcQRWSU5eO81Lj78U34RrVFkOE2n7HHvJzGIckXvK20Dg9P3oo+6huyDi2q3MkakHQENF5FfQiIj4ntO1HAOvD4CvK/jkyukDhx3PDGObvhAprXLnjEi7fhZrJw5lVTyAo2199f5pZUBqsdL/L0X0/9rMbYAQMhMwyo3+bnD81w2Z8ZWWKWG6OWLKfSsUKT6e80OOmNZIoVuC7nJPQ/5v7ui2U5mV4HcqWz05sXciPwIvMzKEKAJHHon91JRWwNp081SPHgoFyESz9aIXioCfES/DY+XaCvFoDFDq+3h6ealHO5F4ZRYG9cDUuXQF/ncoyFX7EHbyfEcZwpqSANSbX0E9xp7hqprgKvk9KPwcLb/yQZsdTo090nvoU7cDk98DV1C4KW1GTfFwmcf0sNTj4ymaF7+AlzkwjTl6d/hPNcGJpY4PYbCm8H

Based on the documentation in https://coq.inria.fr/refman/addendum/sprop.html#coq:flag.Definitional-UIP, it looks like you should be able to define a function `f : seq x y -> x = y` and then you can prove that this function is the inverse of the function `g : x = y -> seq x y`. With this flag on, it should be the case that matches on `f (g p)` will reduce away whenever x and y are definitionally equal, hence avoiding the need to invoke UIP explicitly.

Does this work?

On Sat, Jun 5, 2021, 20:16 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

I just noticed Set Definitional UIP. Is there a way to use this to
avoid needing to define a normal Prop (non SProp) UIP to handle
inversions that result in sigT equalities? Normally, these cases
involve inversion; inversion_sigma; UIP to replace the equality arg of
the eq_rect with eq_refl to allow it to reduce. Do I still need normal
Prop UIP for such cases, or is there a way to bypass it?

[Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions, jonikelee AT gmail.com, 06/06/2021
- Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions, Jason Gross, 06/06/2021
  - Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions, jonikelee AT gmail.com, 06/06/2021
    - Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions, Jason Gross, 06/06/2021
      - Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions, jonikelee AT gmail.com, 06/06/2021
        
        Re: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions, jonikelee AT gmail.com, 06/07/2021