coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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: Thu, 1 Sep 2016 17:46:28 -0400
Authentication-results: mail2-smtp-roc.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-qt0-f173.google.com
Ironport-phdr: 9a23:LnrgjBVGK7ZQ4AB4RD6YxMLhppvV8LGtZVwlr6E/grcLSJyIuqrYZRODt8tkgFKBZ4jH8fUM07OQ6PG5HzFaqs7R+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjYZBwNjz6ga5tzKg+3pEPfrJo4m4xnf4Q2zBLVonJOM8BbxH1lI07byxT74Maz8Zpu/gxfvvsg84hLVqCsLPdwdqBREDlzazN938bsrxSWFQY=

On 09/01/2016 02:24 AM, Jason Gross wrote:

I'm no longer convinced this can be done, but I bet asking on hott-cafe, or
looking at the file PathGroupoid in the HoTT library, could get you ask
answer (the HoTT name for [f_equal] is [ap])

I may try that, as I've hit another road block: types with indices or dependent fields. None of the methods discussed so far work for those, even when using a dependent form of f_equal based on eq_rect. For instance, try to get UIP on Fin from UIP on nat.

-- 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