|
| 1 | +<!--- |
| 2 | +This file was generated from `meta.yml`, please do not edit manually. |
| 3 | +Follow the instructions on https://github.com/coq-community/templates to regenerate. |
| 4 | +---> |
| 5 | +# Paramcoq |
| 6 | + |
| 7 | +[![Docker CI][docker-action-shield]][docker-action-link] |
| 8 | +[![Contributing][contributing-shield]][contributing-link] |
| 9 | +[![Code of Conduct][conduct-shield]][conduct-link] |
| 10 | +[![Zulip][zulip-shield]][zulip-link] |
| 11 | +[![DOI][doi-shield]][doi-link] |
| 12 | + |
| 13 | +[docker-action-shield]: https://github.com/coq-community/paramcoq/workflows/Docker%20CI/badge.svg?branch=v8.10 |
| 14 | +[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI" |
| 15 | + |
| 16 | +[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg |
| 17 | +[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md |
| 18 | + |
| 19 | +[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg |
| 20 | +[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md |
| 21 | + |
| 22 | +[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg |
| 23 | +[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users |
| 24 | + |
| 25 | + |
| 26 | +[doi-shield]: https://zenodo.org/badge/DOI/10.4230/LIPIcs.CSL.2012.399.svg |
| 27 | +[doi-link]: https://doi.org/10.4230/LIPIcs.CSL.2012.399 |
| 28 | + |
| 29 | +A Coq plugin providing commands for generating parametricity statements. |
| 30 | +Typical applications of such statements are in data refinement proofs. |
| 31 | +Note that the plugin is still in an experimental state - it is not very user |
| 32 | +friendly (lack of good error messages) and still contains bugs. But it |
| 33 | +is usable enough to "translate" a large chunk of the standard library. |
| 34 | + |
| 35 | +## Meta |
| 36 | + |
| 37 | +- Author(s): |
| 38 | + - Chantal Keller (initial) |
| 39 | + - Marc Lasson (initial) |
| 40 | + - Abhishek Anand |
| 41 | + - Pierre Roux |
| 42 | + - Emilio Jesús Gallego Arias |
| 43 | + - Cyril Cohen |
| 44 | + - Matthieu Sozeau |
| 45 | +- Coq-community maintainer(s): |
| 46 | + - Pierre Roux ([**@proux01**](https://github.com/proux01)) |
| 47 | +- License: [MIT License](LICENSE) |
| 48 | +- Compatible Coq versions: The v8.10 branch tracks version 8.13 of Coq, see releases for compatibility with released versions of Coq. |
| 49 | +- Additional dependencies: none |
| 50 | +- Coq namespace: `Param` |
| 51 | +- Related publication(s): |
| 52 | + - [Parametricity in an Impredicative Sort](https://hal.archives-ouvertes.fr/hal-00730913/) doi:[10.4230/LIPIcs.CSL.2012.399](https://doi.org/10.4230/LIPIcs.CSL.2012.399) |
| 53 | + |
| 54 | +## Building and installation instructions |
| 55 | + |
| 56 | +The easiest way to install the latest released version of Paramcoq |
| 57 | +is via [OPAM](https://opam.ocaml.org/doc/Install.html): |
| 58 | + |
| 59 | +```shell |
| 60 | +opam repo add coq-released https://coq.inria.fr/opam/released |
| 61 | +opam install coq-paramcoq |
| 62 | +``` |
| 63 | + |
| 64 | +To instead build and install manually, do: |
| 65 | + |
| 66 | +``` shell |
| 67 | +git clone https://github.com/coq-community/paramcoq.git |
| 68 | +cd paramcoq |
| 69 | +make # or make -j <number-of-cores-on-your-machine> |
| 70 | +make install |
| 71 | +``` |
| 72 | + |
| 73 | + |
| 74 | +## Usage and Commands |
| 75 | + |
| 76 | +To load the plugin and make its commands available: |
| 77 | +```coq |
| 78 | +From Param Require Import Param. |
| 79 | +``` |
| 80 | + |
| 81 | +The command scheme for named translations is: |
| 82 | +``` |
| 83 | +Parametricity <ident> as <name> [arity <n>]. |
| 84 | +``` |
| 85 | +For example, the following command generates a translation named `my_param` |
| 86 | +of the constant or inductive `my_id` with arity 2 (the default): |
| 87 | +```coq |
| 88 | +Parametricity my_id as my_param. |
| 89 | +``` |
| 90 | + |
| 91 | +The command scheme for automatically named translations is: |
| 92 | +```coq |
| 93 | +Parametricity [Recursive] <ident> [arity <n>] [qualified]. |
| 94 | +``` |
| 95 | +Such commands generate and name translations based on the given identifier. |
| 96 | +The `Recursive` option can be used to recursively translate all the constants |
| 97 | +and inductives which are used by the constant or inductive with the given |
| 98 | +identifier. The `qualified` option allows you to use a qualified default name |
| 99 | +for the translated constants and inductives. The default name then has the form |
| 100 | +`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the |
| 101 | +`Module.Submodule` namespace. |
| 102 | + |
| 103 | +Instead of using identifiers, you can provide explicit terms to translate, |
| 104 | +according to the following command scheme: |
| 105 | +```coq |
| 106 | +Parametricity Translation <term> [as <name>] [arity <n>]. |
| 107 | +``` |
| 108 | +This defines a new constant containing the parametricity translation of |
| 109 | +the given term. |
| 110 | + |
| 111 | +To recursively translate everything in a module: |
| 112 | +```coq |
| 113 | +Parametricity Module <module_path>. |
| 114 | +``` |
| 115 | + |
| 116 | +When translating terms containing section variables or axioms, |
| 117 | +it may be useful to declare a term to be the translation of a constant: |
| 118 | +```coq |
| 119 | +Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>. |
| 120 | +``` |
| 121 | + |
| 122 | +Note that translating a term or module may lead to proof obligations (for some |
| 123 | +fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to |
| 124 | +declare a tactic to solve such proof obligations: |
| 125 | +```coq |
| 126 | +[Global|Local] Parametricity Tactic := <tactic>. |
| 127 | +``` |
0 commit comments