PUMPKINPATCH的扩展，支持跨类型等价的证明修复_Coq_OCaml_下载.zip

**Coming here from the latest PLDI 2021 draft? The documentation below is meant for users and is a bit out of date. The PLDI 2021 draft code guide can be found [here](./GUIDE.md).** This is PUMPKIN Pi (formerly DEVOID), a plugin for automatic discovery of and lifting across equivalences between types in Coq. PUMPKIN Pi is a part of the [PUMPKIN PATCH](https://github.com/uwplse/PUMPKIN-PATCH) proof repair plugin suite, and is included as a dependency of PUMPKIN PATCH starting with release 0.1. PUMPKIN Pi began as DEVOID, the artifact for the ITP paper [Ornaments for Proof Reuse in Coq](http://tlringer.github.io/pdf/ornpaper.pdf). It has since been extended. A version of PUMPKIN Pi that corresponds to the ITP camera-ready can be found in [this release](http://github.com/uwplse/ornamental-search/releases/tag/itp+equiv). A pre-print of our PLDI 2021 paper [here](https://arxiv.org/abs/2010.00774). Given two types A and B that are related in certain ways, PUMPKIN Pi can search for and prove the relation between those types, then lift functions and proofs between them. The following relations are currently supported automatically: 1. **Algebraic Ornaments**: the type B (like `vector`) is the type A (like `list`) indexed by a fold over A (like `length`) 2. **Records and Tuples**: the type A is a nested tuple of the form `x * (y * ...)`, and the type B is a record with the same number of fields that have the same types 3. **Swapping and Renaming Constructors**: the types A and B are two inductive types that are equal up to swapping constructor order and renaming constructors 4. **Escaping Sigma Types**: the type B (like `vector T n`) is the type A (like `{ s : sigT (vector T) & projT1 s = n}`) escaping the sigma type It then ports functions and proofs across those equivalences. For changes that don't fall into the above four buckets, you need to supply the equivalence yourself in a deconstructed form called a *configuration*. If you need help with this, please check out two examples: switching between unary and binary natural numbers [here](/plugin/coq/nonorn.v), and an easier refactoring of constructors [here](/plugin/coq/playground/constr_refactor.v). Also check out the PLDI 2021 draft [here](https://arxiv.org/abs/2010.00774). # Getting Started This section of the README is a getting started guide for users. Please report any issues you encounter to GitHub issues, and please feel free to reach out with questions. ## Building PUMPKIN Pi The only dependency you need to install yourself is Coq 8.9.1. PUMPKIN Pi also depends on a [Coq plugin library](https://github.com/uwplse/coq-plugin-lib) which is included as a submodule automatically in the build script, and on the [fix-to-elim](https://github.com/uwplse/fix-to-elim) plugin, which is also included. To build PUMPKIN Pi, run these commands: ``` cd plugin ./build.sh ``` ## Using PUMPKIN Pi For an overview of how to use the tool, see [Example.v](/plugin/coq/examples/Example.v) and [minimal_records.v](/plugin/coq/minimal_records.v). ### Overview At a high level, there are two main commands: `Find ornament` to search for equivalences (misleadingly named as an artifact of history and time constraints), and `Lift` (or `Repair` for tactic support) to lift along those equivalences. `Find ornament` supports two additional options to increase user confidence and to make the functions that it generates more useful. If you skip running the `Find ornament` command and just run `Lift` or `Repair`, then PUMPKIN Pi will run `Find ornament` for you automatically first. In addition, there are a few commands that help make PUMPKIN Pi more useful: `Preprocess` for pattern matching and fixpoint support, and `Unpack` to help recover more user-friendly types. The `Preprocess` command comes from our plugin [fix-to-elim](https://github.com/uwplse/fix-to-elim). #### Search See [Search.v](/plugin/coq/examples/Search.v) for an example of search. ##### Command ``` Find ornament A B as A_to_B. ``` This command searches for the equivalence that describes the change from A to B, when the change is supported by automatic configuration. ##### Outputs For algebraic ornaments, `Find ornament` returns three functions if successful: 1. `A_to_B`, 2. `A_to_B_inv`, and 3. `A_to_B_index`. `A_to_B` and `A_to_B_inv` form a specific equivalence, with `A_to_B_index` describing the fold over `A`. For other kinds of equivalences, `Find ornament` returns only the first two of these. ##### Options for Correctness `Find ornament` supports two options. By default, these options are disabled. Together, setting these two options tells `Find ornament` to prove that its outputs are correct. (Also as an artifact of time constraints, the options use the old name, DEVOID.) ``` Set DEVOID search prove coherence. ``` For algebraic ornaments, this option tells `Find ornament` to additionally generate a proof `A_to_B_coh` that shows that `A_to_B_index` computes the left projection of applying `A_to_B`. ``` Set DEVOID search prove equivalence. ``` This option tells `Find ornament` to generate proofs `A_to_B_section` and `A_to_B_retraction` that prove that `A_to_B` and `A_to_B_inv` form an equivalence. ##### Using Custom Equivalences with Automatic Configuration If `Find ornament` fails for an automatic configuration or you would like to use an existing equivalence, you can run this command before lifting (still misleadingly named as an artifact of history and time constraints): ``` Save ornament A B { promote = f; forget = g}. ``` where `f` and `g` form an equivalence that describes one of the supported relations between `A` and `B`. Note that support for this is extremely experimental, and will not yet work if you try this with changes not supported by automatic configuration (you will need manual configuration for that; more below). You can find an example in [TestLift.v](/plugin/coq/TestLift.v). You can also use this to substitute in a different equivalence for an existing equivalence, but again there are some restrictions here on what is possible. See [ListToVectCustom.v](/plugin/coq/examples/ListToVectCustom.v) for more information. You can also skip one of promote or forget, provide just one, and let PUMPKIN Pi find the other for certain automatic configurations, for example: ``` Save ornament A B { promote = f }. ``` This is especially useful when there are many possible equivalences and you'd like to use a particular one, but let PUMPKIN Pi figure out the rest. See [Swap.v](/plugin/coq/Swap.v) for examples of this. ##### Using Custom Equivalences with Manual Configuration To use a custom equivalence not at all supported by one of the four search procedures, like switching between unary and binary natural numbers, check out two examples [here](/plugin/coq/nonorn.v) and [here](https://github.com/uwplse/ornamental-search/blob/master/plugin/coq/playground/constr_refactor.v). These examples set manual configuration and essentially skip the search procedure. We will document them soon! The arXiv paper says a lot about these but the examples are the best place to look for now. ##### Ambiguity Sometimes, automatic configuration of PUMPKIN Pi finds multiple possible equivalences. With swapping constructors in particular, there can be an exponential number of possible equivalences. In the case of ambiguity, PUMPKIN Pi presents up to the first 50 possible options for the user (in a smart order), presents this as an error, and gives instructions for the user to provide more information to `Find ornament` in the next iteration. If the equivalence you want is not in the first 50 candidates, please use `Save ornament`. See [Swap.v](/plugin/coq/Swap.v) for examples of both of these. ##### Tactic Support PUMPKIN Pi produces tactic suggestions for all proofs that `Find ornament` finds. These are experimental, especially with dependent types, but may help you work with tactic proofs about equivalences. You should think of these