coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq

From: Alyssa N Byrnes <abyrnes1 AT cs.unc.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq
Date: Thu, 27 Sep 2018 09:54:33 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abyrnes1 AT cs.unc.edu; spf=Pass smtp.mailfrom=abyrnes1 AT cs.unc.edu; spf=None smtp.helo=postmaster AT mail-yb1-f173.google.com
Ironport-phdr: 9a23:/tROFx8cDoemzf9uRHKM819IXTAuvvDOBiVQ1KB31+scTK2v8tzYMVDF4r011RmVBdqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/0hykIODE3/nzZhM9+jK1ZvhyvoAdyw5LNYIGQKPZ+fr/RcNEcSGFcXshRTStBAoakYoYTC+oAPf1Yr5LnqFATtRW1GBShBeP1yj9OmHD2xrAx3uM7Hg7d3A0gBdQOv2rPrNnoL6odTfu1wLPVzTXFc/xawyny55XVch04p/yHQLx+cc3UyUY1FgPFiE2dqY3jPzOP1+QCqXKX7+R6Ve63hG4nqh1xojiyxsg3kIXGmoUVylXC+C5kw4g1PcW1RFBnbdOgCpddtCGXO5FoTs8/R2xkojs2x78ItJKjYiQHyYgrywLaZvCab4SE/h3uWeOKLjtkmH5qYreyihKv/kiuxO3xU8u530pRoSVYl9TAqHAA2hLT58WCUPRy4lmt1DeK2g/J6uxLP0Y5nrfBJZE72L4/jJ8TvFzDHiDonEX2i7ebdkA+9eip7+Tre7XnqYSBO4NthAHyL6Yjl8KlDeQ3NQgOWGeb+eCi27H54UL5R7BKguU3kqnfrp/aOdwWqrClDwJRyIou6BayAy243NgFmXQLNk9JdRCJgoTxPlHBOvH4DfOxg1S2lzdrwujLMaf6DZTNNHjDlqnufa1g50NH1AUz1spT549SCr4dOv78RFL+tMHAAh8jLwO02/rnCMl61o4GRW2PBbaZPLrOvl+M++IgOPKBZJQVuTb4M/gq/eTijX4/mV8HfKmmx4EbaH6iHqcuH0LMan31x9wFDG0ivwwkTeWshkfRfyRUYiObW7Mn/ThzLsqMHJ3FS5vl1LWLzT29E4YPTmtdTE2KGjHle5jSCKREUz6bPsI0ym9MbrOmUYJ0jUj/5j+/8KJuK6/vwgNdsJvi0NZv4OiKz0M57nppCc/b3m2QHTgtwjE4AgQu1aU6mnRTj0+Z2PEi0fdDU8FV7LVEXhpobceBndw/MMj7X0f6RvnMSFuiRY/4UzQ4T9Z00tVXJkgkRI7kgRfE0C6nRbQSku7TCQ==

This is very helpful. Thank you!!

Alyssa Byrnes

> On Sep 27, 2018, at 9:48 AM, Pierre Courtieu
> <pierre.courtieu AT gmail.com>
> wrote:
>
> Hi,
> It depends what kind of sets you want.
>
> 1) you need to reason about infinite sets? If yes then Ensembles
> (+Classical_Sets?) is about everything you have got afaik, in
> particular you lose induction principles.
>
> otherwise:
> 2) Do you want to suppose a decidable equality over elements? If you
> want to really compute on them at some point you probably do.
>
> If yes: you can use MSetXXX functors of the standard library. Lots of facts.
>
> otherwise:
> - Library Finite_sets + Finite_sets_facts which are built upon Ensembles,
> - https://coq.inria.fr/library/Coq.Vectors.Fin.html#t represents
> finite sets as segment of integers of the form :[1..n].
> - https://github.com/aspiwack/finset another representation using numbers
>
> There are probably much more.
>
> Hope this helps
> Pierre
>
>
>
> which represents sets of consecutive integers [1..n]
>> Le jeu. 27 sept. 2018 à 15:02, Alyssa N Byrnes
>> <abyrnes1 AT cs.unc.edu>
>> a écrit :
>>
>> I'm looking to work with and reason about unordered sets of an abstract
>> variable.
>>
>> For example, I define variable a as:
>>
>> Variable a : Type.
>>
>> I know I can use Ensembles, but the Ensembles library doesn't have a lot
>> of supporting theorems. Are there any other libraries I can use?
>>
>> (If you have a suggestion, could you please show an example of how you
>> would instantiate one of these sets?)
>>
>> Many thanks!
>> Alyssa Byrnes

[Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq, Alyssa N Byrnes, 09/27/2018
- Re: [Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq, Pierre Courtieu, 09/27/2018
  - Re: [Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq, Alyssa N Byrnes, 09/27/2018