coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] is there a way to use Definitional UIP to avoid needing Prop UIP for inversions
Date: Sat, 5 Jun 2021 20:15:38 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f45.google.com
Ironport-hdrordr: A9a23:3Awri6OQ9694psBcTvCjsMiBIKoaSvp037BN7TELdfU1SL3hqynKpp4mPHDP+VUssR0b6LK90cq7MArhHPxOkO4s1N6ZNWGM2FdARLsC0WKI+UyFJ8SRzJ856U6iScRD4R/LYGSSQfyU3ODBKadH/DBPys6Vuds=
Ironport-phdr: A9a23:a6cFVBKqIKXbAtvrXdmcuMlmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCGtLM21ASCBNuBo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/229pHJbQhEmDSwbbxvIBi3swnaq9Ubj5ZlJqst0BXCv2FGe/5RxWNmJFKTmwjz68Kt95N98Cpepuws+ddYXar1Y6o3Q7pYDC87M28u/83kqQPDTQqU6XQCVGgdjwdFDBLE7BH+WZfxrzf6u+9g0ySUIcH6UbY5Uimk4qx2ShHnlT0HOiY3/m/XlMJ+kaFVrhWuqBNjzIDZe52VOfhkc6/BZ94WWXRNU8BMXCJBGIO8aI4PAvIPMeZaqIn9oVoOrRigCgmoGuzg1CRFhnDz3aIg0uQhFRvK0xAnH9ILvnjfsdL4NKUVUeCzzanIzivMb/dI1jjj84XIfRUhruuNXbJ0a8be1U4vFwbcg1iWtIfqMC+b2P4XvGiH8+pvS/ivi2g/pg1sojWhxsghh5fVio8Jyl3J9yt0zZo6KNGkSEN3fNCqHIdUuiybN4V7Qd0vT310tSsn1LELu4K2cTUExZknyRDSbeGMfYuQ4h/7SuqdPTN1iGhmdb+/nRq+71Wsx+nmWsS70FtGtjRJn9jQunwQ0hHf98yKRed480qu2DuDyxzf5+RZLUwqiabWLposz7E+m5cctEnMAzT5mEv4jKKTeEUr5Oil5Pjib7r6qZKRNJR7hwfjOao0gMO/G/43Mg0WUmib5+u80Lrj8FX8QLpQj/02lrDVsInEJcgGv6K5DQBY34Y55xawCDem19sYnX0ZI15fZB2HiI3pN0nPIPD+E/i/n0yhnCl3y/3CJLHsAZXAImLdnLv8ebtx8UFRxQorwdBa/Z1UC7UBIPzpWk/2sdzVFh05Mwuyw+bmC9VyyIceVnyRDaKCP6PStEWH5uMrI+WWeIAVvzP9J+A/5/HylX85hUMdfa6x0JQLb3C4B+1qLFmdYXrxmdgMCnwKvwo7TOzyklKOSz9TZ3CoX6I9/D43EoymDZ2QDryq1beGxWKwGoBcLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO3rSYgn1BKjsAL347ViJ+vQvCYfsNirgNpy4ezQmBU/+BR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6Ut25Sw9PRW7vJNFx4kbNvSk7E8BNf1VQbMONyOTQT+Kj1JKT40R9M1hdQJZhQkcz1Hph/G1iuuRbQSku7TbKE=

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