coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] help with automating derived UIP_refl proofs
Date: Sun, 28 Aug 2016 18:55:57 -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-qk0-f180.google.com
Ironport-phdr: 9a23:9ej6oRxIMFJAcvvXCy+O+j09IxM/srCxBDY+r6Qd0e8fIJqq85mqBkHD//Il1AaPBtSCra4fwLON6OigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJVkTz2PmOvsydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+vh7aCACL+3E0U2MMkxMODRKWwgv9W8LTtS3zqup03mG+MMzoQLYoEWCg6KFqSxLshSovODsw8WWRgct12vEI6Cm9rgByltaHKLqeM+BzK/vQ

On 08/28/2016 03:44 PM, Adam Chlipala wrote:

I think proving this kind of goal is simpler via first building a library of theorems for porting UIP between types, like so:

Yes! Thank you! I don't think the way I was progressing would have ended up this well.

-- Jonathan

[Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 08/28/2016
- Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 08/28/2016
  - Re: [Coq-Club] help with automating derived UIP_refl proofs, Adam Chlipala, 08/28/2016
    - Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 08/29/2016
    - Re: [Coq-Club] help with automating derived UIP_refl proofs, Dominique Larchey-Wendling, 08/31/2016
      - Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 08/31/2016