coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative Set

From: Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Impredicative Set
Date: Fri, 15 Mar 2019 23:16:46 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jean-francois.monin AT univ-grenoble-alpes.fr; spf=Pass smtp.mailfrom=jean-francois.monin AT univ-grenoble-alpes.fr; spf=None smtp.helo=postmaster AT zm-mta-out-1.u-ga.fr
Ironport-phdr: 9a23:+8sHXhHpeMOv45S6ljaRJZ1GYnF86YWxBRYc798ds5kLTJ7zr8SwAkXT6L1XgUPTWs2DsrQY0rKQ6/mocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSaxbaluIBmrsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOTA5/m/Jl8J+j6xbrx29qBNizIDbYo+aOeFifq7eZ94WWXZNU9xTWiFHH4iyb5EPD+0EPetAq4fyuUEBrR2nCQesHuPg0DlIiWPx3a07yOQqDAbI3AsmH9IPtnTfsdL4NKUMXu+vyqnE1DvDb+lM1jf79IfIdREhoeqWUbJ1dsrRz0gvFwXeg1WNr4zlPi2V2v0Cs2iB8eVgU+WvhHUjqw5vuzSg3MMsipHXiYIO0FzE+z95zZ8zKNalRkB7ZtukH4FRtyGcL4Z2TcIiQ31ouCYn0bIKo4K0fC8PyJkh2hXRaOSHfpCV7h/jSuqdOzV1iXB/dL6hmxq+7VKsx+39W8Ws1FtGsjBJn9bSunwX1RHf99KLRuZ880u83zuEyhrd5fteIU8ukKrWM54hzaA0lpoUqUnCHyr2lFzzjK+KbEoo4++o6/n7Yrn/u5OQLZJ0hhjxMqs0gMC/D/44PhAPX2id5+u8yKXu8VD5TblUlPE7kKvUvIrEKcgHuqK1GQ9Y34c75xa6FTim0dAYnXcdLFJCfRKKl4rpNE/UL/D+FPu/jU6sny1tx//aOb3hA47NImLGkLfme7Z96khcxREuzdBZ5pJUFKgNIP3pWkDvstzYCQQ2MwiqzOr+Etp90pseVnyUAqODPqPSq0eE5vgzLOmUeI8VpDH9JuA56P7plH81gEMSfa203ZQMc324BfRnI0CBYXX2mNsBEGEKvhA/TOPwklGCXyRTND6OWPc34Sh+A4a7B6/CQJqsifqPxnSVBJpTM0JLA1bJP23hcY6DWuxETSWUI8kpxj4JXL7kRZUo0xqptRS8zr1hL+z85ysZq9fsztVz4OfXmFQ78SR5FIKTyTfeHClPgmoUSmpuj+hEqktnxwLbiPkqs7ljDdVWoshxfEI/PJ/YwfZ9DoquCB/Hf8nMR0yrRNKsBTx0R9YpzsRIbVwvQoz+3CCG5DKjBvour5LOHIY9qP6Own7wOYNy0XvA06MlghwvRtNCLiuonPwnrlWBN8vyi0yc0p2SW+Ec0SrKrj3R32/LuV1RFQltTeCcG21aaUKQo86rvk4=

I just completed comments of PM Pedrot in
https://github.com/coq/coq/issues/9458

In short, impredicative Set is useful when considering extraction
of programs in CPS style (at least, very natural for patterns
corresponding to exceptions).

Jean-Francois

On Fri, Mar 15, 2019 at 09:29:21PM +0100, Théo Zimmermann wrote:
> Related: [1]https://github.com/coq/coq/issues/9458
> Le ven. 15 mars 2019 à 20:26, Stefan Monnier
> <[2]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