coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?
Date: Fri, 15 Feb 2019 09:07:35 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f175.google.com
Ironport-phdr: 9a23:xNW/MB/BIEABtP9uRHKM819IXTAuvvDOBiVQ1KB42+IcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1HrxysvAB/w5fObY2JKPZyYqHQcNUHTmRBRMZRUClBD5uhYoQVFOoKIPtWr5H8p1sSsRuxGxOsBPjywTJPnXD6x7c13/4vEA3cxwwgB9MOsGjIrNrrLqcSSvu4zKbNzTrZbvNW3S3x55TPchAkuPyBW697f8TWyUkqDQzFj1OQpJTqPzOUyuQNs3Wb4PF6We2zjG4nrgd8qSWsyMc0koTFmJ4Zx1Te+Sh6wIs5P8O0RFN/bNK+DZddtSGXOo1rSc04WW5oojw1yrgetJ67YicKzJMnygbaa/OdcoiI5gvvVeaKLjtlnX5ldq+zihSy/ES6xe38Uc600FlOriVbiNXDqncN1xnL5siGTPty4Fuh1C6R2wzP7uxIO0M5mKrBJ5I/37I9koAfvVnBEyL2gEn2ibWZdkQg+uim8eTnZbDmq4eHOINukA7yKKovltakAeQgMwgOQ3Sb9vqm1L345kD5T7BKgec3kqndqpzVOcMbpquhDw9Pzokj8wq/Dyuh0NkAgXYHK0tFdAubgIjtJlHBO+v1Dey/glSpiDdk3erKPrznApXXL3jMiq3tfbhn6x0U9A1m79lE4JQcT4MBJ/T8EnTxudrXS1cZLkTgzernGs4njtpGcWKIHqqQMaeUuliNsLEBOe6JMaUco37GM/k5+/P0ljdtkxkUO7bvxoMWdGy1BO9OLECQYH6qidAERzRZ9jEiRfDn3QXRGQVYYGy/Cvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPzkUBVWFEHOufIKBCa5VNHCiZ/R5mzlBboCPDpc73Ej35gD/wrtjaOHT/39A7M+x5J1O/+TW0CoK23l0AsCaiT/fSmh1miYZTWZz0vkg/ApyzVCM1aU+iPtdR4Re

Could you be more precise what are you looking for? Large parts of the
stdlib are constructive, so I assume you're looking for something
specific.
Also, there are at least two ways to work constructively in Coq.
Propositions as Types, and Propositions as Props.
One can even use a mixture of the two.

Which one would you like to use?

On Fri, Feb 15, 2019 at 1:37 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

[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