coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] help with automating derived UIP_refl proofs

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] help with automating derived UIP_refl proofs
Date: Thu, 01 Sep 2016 03:18:37 +0000
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-qk0-f181.google.com
Ironport-phdr: 9a23:lcx2LhWevsqFSZxVsDcVZLI/mJ3V8LGtZVwlr6E/grcLSJyIuqrYZhGDt8tkgFKBZ4jH8fUM07OQ6PG5HzFYqsnf+DBaKdoXBkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2asc272qiI9oHJZE0Q3XzmMOo0cU398luZ9pFPx9AzcuBpklqBi0ALUtwe/XlvK1OXkkS0zeaL17knzR5tvek8/dVLS6TwcvdwZ7VZCDM7LzJ9v5Wz5lGQBTeIs3AbSyAdlgdCKwnD9hDzGJnr4QXgse8o+iCBOsu+YqozQi/qu6ViUxjuhz0ALCVo2G7Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZCSA==

Actually, I think it's possible to do better; you should only need AtoB_BtoA specialized to the point you care about. This should be a relatively simple transformation to make, and, I think, should be powerful enough to let you handle recursive types

On Wed, Aug 31, 2016, 8:05 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 08/31/2016 07:46 PM, Jason Gross wrote:
> Here's the pointed version of UIP-respecting-isomorphism:

Thanks, Jason!

-- Jonathan

Re: [Coq-Club] help with automating derived UIP_refl proofs, Dominique Larchey-Wendling, 09/01/2016
- Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
  - Message not available
    - Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
      - Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
        
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jonathan Leivent, 09/01/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Jason Gross, 09/02/2016
        Re: [Coq-Club] help with automating derived UIP_refl proofs, Dominique Larchey-Wendling, 09/08/2016