coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Subject: Re: [Coq-Club] Purely constructive utility libraries in Coq?
Date: Tue, 26 Feb 2019 14:25:13 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:bhBJXxLtLET0uB2k49mcpTZWNBhigK39O0sv0rFitYgRLfjxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNxzJXZYJ2XOfdkYq/RYd0XSGpHU81MVyJBGIS8b44XAuQdJ+lYq4f9rEYKoxujAwmsC/7kxzhKhn/r26063P8sEQTe3AwhBt4Oq3rVrM7vOKcVS+C1w7DFwDPeZP1Y3jf97ZLHchEnofyUWLJwacvRxVA0FwLLlVWcs4vlPyma1ukLrmOV7PJgWPqyh2Mprwx9uCWjy8M2hoTKh48Z0F/J+TlhzIooK9C1TFR3bcOgHZdKqi2XNoh7TtkgTmxrvisx16cItoShfCcQzZQq3x7fZOKDc4iP+h/jVvuRITF/hH5/fbK/nxey/VGjyu34Tcm7y0xGri9dktnDrHwCygLc5tCGSvt74EihxS6C2x3d5+xAO0w4iK7WJ4Qiz7MxjJYevljPEjfzmErsja+Wcksk+vKv6+TierjmpIKcN4l7igzlN6Qugs2/Df0jMgkARGiX4+O81Kfs/UHhWrVFkuU2krXFsJDdPckUuqm5AxZM3ok/7xa/Eiyp3c8DnXgHKVJFYAiIg5LoO1HIOvD4DO2wj06ikDdxlLj6OejqBYyIJXzemp/ge6x84ghS0k5779lE4JQcT4MBJ/T8EnTxudrXS1cZLkTgzernGs4njtpGcWKIHqqQMaeUuliNsLEBOe6JMbUcvDi1CeUj6La6j2I/lncYZajsxoQMLneiEaI1cA2ifXPwj4JZQi8xtQ0kQbmy0QzQYXtof3+3GpkEyHQ+AYOiA53EQ9n20rmZ3WKgAYYQYXpJWAnVTSXYMr6cUvJJUxq8Z9d7m2VfB725Sso6ygrosxX1meI+c7jkvxYAvJem7+Bbou3ekRZor252EsKalWSVTiR3mngCATou0+ZzrB4lxw==

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.

std++ has (purely constructive and still extensional) implementations of
finite
maps and finite sets, maybe those are helpful for you:
<https://gitlab.mpi-sws.org/iris/stdpp/>

; Ralf

[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