coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative Set

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Impredicative Set
Date: Fri, 15 Mar 2019 21:29:21 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f48.google.com
Ironport-phdr: 9a23:pr4/DhWCKlCbi0A4zoPMX8QRutfV8LGtZVwlr6E/grcLSJyIuqrYYx2Ft8tkgFKBZ4jH8fUM07OQ7/m4HzRZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5uIBmssQndq9QdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZDYy8YYkAAeoPM+hbsofzuUcBoACkCgWwHu7i0CNEimP00KA8zu8vERvG3AslH98WrnrUrM/yNKAKXu+2zanIyDDDYO1M2Tf48ofIdBYhquyLULJsccre104vGxnEj1WRrIzlOjKV2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTHiIISz1DL7yR5wIAtKN23SU57fd6kEIZLuC2AK4R2RcYiTmd1syg50r0LoYC3cDQOxZg9xBPSa+aLf5aV7h/hTuqcLjR1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HJtn8X1hzT7tGLSuVm/ku8wDqP2Q/e5+JeLUA7kqrbLJEhwroumZYJrUvDGSr2lF33jK+QaEok5vCl5/r7brjivJORNI95hhvgPqgzmMGzG+s1PwsWU2ie4+u81bnj/UPjQLVNi/07irXZsJDEKsQcvKK4Ag5V0oMm6xa+FDqm39EYkmMGLFJBYh6Ik4/pO1TWLPDiEfi/m0iskCtsx/3eIrLhBYzNImHfn7flYLZy8FVRyBEzzNBa/5JbEKsNIPP1Wk/rtdzXFAU1MwKuw7WvNNIo/YQHEUmLH6XRZKjVqBqD4v8lC+iKfo4c/jjnfasL/fnr2EM5GFgqT6is2JYNbXm+GLwyP0WUZjz+g9IEEE8FuwM/SKrhj1jUAm0bXGq7Q69pvmJzM4mhF4qWA9n12OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVMXCdJ8ZglnoPUr3zEtZ9hyHrjxfzzv9cFsSR4jcR7Mux29185umVnhY3p2QtUpatllqVRmQxpVsmAj872Kcl/B54w1aHlLZj2rlWSYwV6PROXQM3c5Xbyr4iBg==

Le ven. 15 mars 2019 à 20:26, Stefan Monnier <monnier AT iro.umontreal.ca> a écrit :

> 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