coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq
Date: Thu, 27 Sep 2018 09:02:34 -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-f169.google.com
Ironport-phdr: 9a23:B7/AFh3hjBEvU8mOsmDT+DRfVm0co7zxezQtwd8Zse0eK/ad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDsIOTE2/2/KicJ+grxVrhW6qhxj2o7UZZ2ZNPpicq/De94RWGpPXtxWVyxEGo6xc48PDuoaPeZDtYb2ukMApgajCAisHuPvzCFHhmTr1qA9yesuCgHH3BYmH90Qq3TYsc74O7sJUeyv0anIyynMY+lI1jjg9YjFaxYsquyPU7Joacfd11UjGgffgliTqYHpJS2Z2vkJvmSB8uZtVOaih3Y5pwxwvjSj2MIhh4fVio8Uz13J+z92z5s2KNC9R0N2ZcOoHIdVuiyZOIZ6Xt4tTmRntSkn1rIJp5u2cDUIxZkn2hHSbuKLfoyT7RLtUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtKqzBKktjItnwU1x3c8dWLRuJz/ku82DuC0xrf6u5DIUAzmqrbL4AuzqQsmZoUtETPBi72mEPog6+Kbkgo5PSk5uD9brjlppKQLZF4hhz6P6g0h8CyAOA1PhALX2eB+OS80LPj/Vf+QLVPlvA5iLLWsZDAJcQduKG5GBJZ350/5BakFTumzdIYkmUdIF1bZR2HkpDlO0vSL/DgEfe/n1OsnS93yPDBJ73tG4nCLnzekLj6Zrt98E5dyA8rzd9F/Z5UC7cBIOjyWkDrrtDYAAU5YESIxLPsD8w43YcDU0qOBLWYOeXcqwym/OUqdsCIdZQOsX7bY9I0/fjjljdtkFUMZ6+kxsI/Y2v+A/JtZUiVfCy/0Z86DW4Ws19mH6TRg1qYXGsLPifgb+cH/jg+TbmeI8LGT4GpjqaG2X7hTJZNIH1AARaBHWq6LtzYCcdJUzqbJ4paqhJBTaKoEtVz3groqQnxjbdrM7iMo3BKhdfYzNFwotbru1Qy+DhzVZrP1miMSyRllDpNSWZojeZwpktyzlrF2q990aRV

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