coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Purely constructive utility libraries in Coq?

From: Abhishek Kr Singh <abhishek.uor AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?
Date: Fri, 15 Feb 2019 09:31:04 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.uor AT gmail.com; spf=Pass smtp.mailfrom=abhishek.uor AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f44.google.com
Ironport-phdr: 9a23:WmfwExBzxQ6GamV8XvugUyQJP3N1i/DPJgcQr6AfoPdwSPvyocbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YCE/EOPeZZr4nmp1sBsxi+DhSpCuP11zRGm3723as10+QhDArL2xYvEMkOsHTVt9X1NLkdUeOvwKnVyjXDdehb2Tj46IfScxAhpeuAUq53ccrU0EQiER7OgFuXqYzgJTyV1+INvnCU7+phSeKvi3MnpBprrjezwccsj5HFhp4UylDK7yV12pw1KsOjSEJhYN6kFoNctzuEOIttWM8uWWBouCA8x7YbupC7ZDAHxIo7yxPbcfCKcIiF7gj9WOqPPzt0nn1odb25ih2v60av0Pf8WdOx0FtSripKjN3MtncV2hzW8MeHS/998l682TmVygzf8+9ELE87mKbBJJ4hxbkwlpUXsUvdBCP5hEL2jKqOekUl/Oin9fjnb634qpOAM4J4kALzP6Q0lsChH+g0LBICUmeU9Oik0b3s50z5QLFEjv0slanZtYjXKt4Aqa65Ag9VyYYj5Ai8Dzu8zdQYmmMHIUlKeBKClYfpOlXOLOrkAve4hlSgiC1ryOzePr39HpXNKWDOn6vmfbZk8kJT1A4zzc1E6J9PEbEAIPfzWlfru9DCDx85NRa0w+f9B9ln2IMeQzHHPqjMO6TL9FSM++gHIu+WZYZTtiyuBeIi4qvHh384gl8QfuGKx9MsaXa3HrwyKk+ZYGHsj9RHDGAQlgU7Re3uzlaFVGgAND6JQ6sg62RjW8qdBoDZS9X12e3T7GKABpRTI1t+JBWJGHbseZ+DXq5VOi2XK85l1DcDUOr4EtNz5VSVrAb/joFfAK/M4CRB7MDs0dF046vYkhRgrWUpXfTY6HmESiRPpk1NRzIy2/oi80l0y1PGzKEhxvIESZpc4PRGVgp8PpnZnbR3

Dear Jason,

You might also find our library useful if you only want to reason about finite collections.

https://github.com/Abhishek-TIFR/List-Set

It is fully constructive and have most of the elementary results on sets, power set and functions available. You may specifically look at the files: SetSpecs, OrdList, OrdSet, SetMaps and Powerset.

On Fri, Feb 15, 2019 at 6:08 AM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

Hi Bas,

do you mind pointing out which folder I should look at? I try to search but the folder structure doesn't look straightforward to interpret.

Sincerely Yours,

Jason Hu

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Bas Spitters <b.a.w.spitters AT gmail.com>
Sent: February 14, 2019 11:36 AM
To: Coq Club
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?

The corn library has some of the features your looking for:
https://github.com/coq-community/corn

On Thu, Feb 14, 2019 at 5:26 PM Jason -Zhong Sheng- Hu
<fdhzs2010 AT hotmail.com> wrote:
>
> Hi,
>
> I am wondering is there any purely constructive libraries in Coq out there, that can serve as a stdlib alternative?
>
> I am aware of those mathematical libraries that are purely constructive. However, those libraries tend to focus on mathematical problems, instead of collections, their properties, etc, that are more based on utilities, e.g., Forall, Exists, In, etc that are defined in Type.
>
> Sincerely Yours,
>
> Jason Hu

Thanks and Regards.

Abhishek Kr. Singh,
Research Scholar, STCS, TIFR Mumbai.

Mob: 9867579837
Homepage: http://www.tcs.tifr.res.in/~abhishek/

http://www.tcs.tifr.res.in/people/abhishek-singh

[Coq-Club] Purely constructive utility libraries in Coq?, Jason -Zhong Sheng- Hu, 02/14/2019
- Re: [Coq-Club] Purely constructive utility libraries in Coq?, Bas Spitters, 02/14/2019
  - Re: [Coq-Club] Purely constructive utility libraries in Coq?, Jason -Zhong Sheng- Hu, 02/15/2019
    - Re: [Coq-Club] Purely constructive utility libraries in Coq?, Abhishek Kr Singh, 02/15/2019
    - Re: [Coq-Club] Purely constructive utility libraries in Coq?, Bas Spitters, 02/15/2019
- Re: [Coq-Club] Purely constructive utility libraries in Coq?, Ralf Jung, 02/26/2019