coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative Set

From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
To: Jay Kruer <kruerj AT reed.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Impredicative Set
Date: Fri, 15 Mar 2019 15:25:05 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT pruche.dit.umontreal.ca
Ironport-phdr: 9a23:SYwsExeohGFjy9ifH86VMR4MlGMj4u6mDksu8pMizoh2WeGdxcS6bB7h7PlgxGXEQZ/co6odzbaP6+a4ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfb9+Ngm6oRjMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyxPDJ2hYYUMAeoPM+RXoIfyqFQSohWzHhWsBPr1xzNUmnP7x6833uI8Gg/GxgwgGNcOvWzJotXpKqgSX/q6zK/VxjvEaPNW3zH96InWfRA7vPqBWrdwcc3XyUkpFgPKkE+QpJfmMT2Jz+oBqWaU4e1nVeKpl24nsR9+rSKrxss2lITEmpsYx1bZ/it62IY4PcC0RUBlbdK+Dpdcqy6XO5FoTs4tQmxkojg2xqMetZKmciUG1o4rywDDZ/GIaYSE/BDuWPyPLTp3mn5ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrmgN1wbO6sebSvty4F2t1iuO1wDP8O1EPEU0la3dK5492L4/iIAcsUDZEiDqgkr6lK6WdkM69ei08+nrf7vrqoGGO4Nqlg3zPb4iltKwDOk5KAQCQXaX9fy51LL5/E35RLtKjucxkqncqJ3aIMMbpqi/Aw9UzIkj8Q2yDza80NQfh3UHMVdFeBWBj4j1IVHBPur3DfOlj1uwijhn3+rGMaH5ApXRMnjDl6/scqp6605F0QY80dRf549PBbwaO/LyWkrxtMTCARMjMgy0xfznCNRn2Y8EV2KPGPzRDKSHk1aZrsE1PuSWLNsWoivwMfoN/fPjgTk0lUJLLoez2p5CU2y1EP1ga2CeZ3ztj81JRWINuAw/QfbCqWelFwN2YHCuRa814ncQIdT1Xs/4WomxjenZj2+AFZpMazUDUwjUSCa6R8C/Q/4JLRmqDIpkmz0AW6KmTtZxhxC0s0nnzr1hMvDZ8ylevpuxjYEptd2Wrgk78HlPN+rYy3uEFjEmv1kvAQIT26Zju0F0zhGo+Pog2qEKJZlo//pMFzwCG9vcwuh9UY2gQhjcddeEDlqnXpO7BDY3Usg8yttIaE8vQ9g=

> I am wondering how “sketchy” the use of impredicative Set in Coq
> developments is considered.

I'm not in a position to weigh in on this aspect, but my experience with
it has been rather disappointing: the restrictions imposed on it to
avoid inconsistencies (namely the inability to perform strong
eliminations on such large Set types) renders them frustrating, because
you can define interesting datatypes and functions on them, but very
often you can't then prove properties of those functions (at least not
without adding ad-hoc axioms whose soundness is at best unknown).

Stefan

[Coq-Club] Impredicative Set, Jay Kruer, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Stefan Monnier, 03/15/2019
  - Re: [Coq-Club] Impredicative Set, Théo Zimmermann, 03/15/2019
    - Re: [Coq-Club] Impredicative Set, Jean-Francois Monin, 03/15/2019