Welcome to the PUMPKIN PATCH proof repair plugin suite! This plugin suite is a collection of plugins for maintaining proofs as specifications change over time:
- PUMPKIN PATCH (paper, talk video): example-based proof repair
- PUMPKIN Pi (formerly DEVOID) (ITP 2019 paper, standalone plugin, ITP 2019 talk video, PLDI 2021 draft): proof repair across type equivalences (originally just a specific case of this, but since extended)
In addition, this plugin suite includes some development tools, like the fix-to-elim plugin for automatic fixpoint translation, that may be useful for plugin developers and Coq contributors more broadly. We discuss these briefly at the end of the document.
All of these tools, including DEVOID, are included as dependencies of the main PUMPKIN PATCH plugin, so you can use both at the same time. More information on using PUMPKIN Pi (formerly DEVOID) can be found in the the standalone plugin repository. The remainder of this document will focus on how to use the main PUMPKIN PATCH plugin. We hope to add an example of using these both together soon.
This is a prototype plugin for finding patches for broken Coq proofs. To use PUMPKIN, the programmer modifies a single proof script to provide an example adaptation of a proof to a change. PUMPKIN generalizes this example into a reusable patch which can be used to fix other broken proofs.
Reading the paper may help if you are interested in understanding the internals of the tool. The paper links to a release that captures the code as it was when we wrote the paper. The talk video may also be helpful.
The plugin works for Coq 8.9.1. There are branches for Coq 8.5, 8.6, and 8.8, which we are no longer maintaining.
cd plugin
./build.sh
If you would like to use PUMPKIN in all of your developments, add this line:
Require Import Patcher.Patch.
to the beginning of your coqrc resource file. Otherwise, you will want to write this line whenever you use PUMPKIN within a file.
We will walk through a simple example. You can follow along this example by looking at the code in Example.v.
Suppose you have proven a theorem old1:
Theorem old1:
forall (n m p : nat),
n <= m ->
m <= p ->
n <= p + 1.
Proof.
...
Qed.
You then realize that the conclusion of old1 is weak, so you strengthen it
to the theorem new1:
Theorem new1:
forall (n m p : nat),
n <= m ->
m <= p ->
n <= p.
Proof.
...
Qed.
You would like to port a proof that applies old1:
apply old1.
To instead apply new1:
... apply new1.
To do this using PUMPKIN, load the file Example.v (feel free to use your favorite IDE here instead of coqtop):
coqtop -load-vernac-source plugin/coq/Example.v
Next, import the plugin:
Require Import Patcher.Patch.
Invoke the plugin to produce a patch:
Patch Proof old1 new1 as patch.
This defines a term patch. Let's check the type of patch:
Check patch.
This should produce this output:
patch
: forall n m p : nat, n <= m -> m <= p -> n <= p -> n <= p + 1
In other words, patch is a function that takes the conclusion of new1 back to the conclusion of old1.
Then anywhere we have a proof that applies old1:
apply old1.
We can use patch to port this proof to use new1 instead:
apply patch. apply new1.
Within a proof, you can run the tactic:
patch old new as h.
to add a new hypothesis h to your proof state. This has the same functionality as the command version for
now, but will eventually suggest new tactics directly.
One thing that you'll notice is that in the example above, we applied this patch by hand. For now, PUMPKIN does not automatically apply patches that it finds. We are working on a better user experience.
In the meantime, we suggest adding patches to a hint database. For example, instead of writing this:
apply patch. apply new1.
You can instead add patch to your hints:
Hint Resolve patch.
You can then port your proof to use new1 with no additional changes:
apply new1.
The PUMPKIN-git interface searches for patches across Git revisions. It also automatically removes the reference to the old definition. Please see the repository for more details.
By default, PUMPKIN has very limited support for proofs that use pattern matching and fixpoints.
However, the Preprocess command by Nate Yazdani automatically converts simple pattern matching and fixpoints
into induction principles, which PUMPKIN does support. You can Preprocess individual proofs:
Preprocess old as old'.
Preprocess new as new'.
Patch Proof old' new' as patch.
Or you can preprocess entire modules:
Preprocess Module Old as Old'.
Preprocess Module New as New'.
Patch Proof Old'.old New'.new as patch.
See Preprocess.v and PreprocessModule.v for examples
of how to use these commands. There are also proofs in Regress.v and IntegersNew.v
that demonstrate its use with Patch Proof.
This command is available as a standalone plugin as well, if you are interested.
For some kinds of proofs, PUMPKIN needs extra guidance to search for a patch. The hope is that this will eventually be unecessary, but for now, it is a way to work around limitations in the tool.
You can provide this guidance by cutting a lemma. For example, consider the proofs of bin_to_nat_pres_incr in Induction.v. These proofs each
contain proofs of inline lemmas:
assert (H : forall a :nat, S (a + S (a + 0)) = S (S (a + (a + 0)))).
assert (H : forall a :nat, S (a + S a) = S (S (a + a))).
PUMPKIN cannot yet automatically determine that the patch between the versions of bin_to_nat referenced
by each bin_to_nat_pres_incr is in the difference of this inline lemma.
However, we can guide it there:
Definition cut :=
forall (a : nat),
S (a + S a) = S (S (a + a)) ->
S (a + S (a + 0)) = S (S (a + (a + 0))).
Patch Proof blindfs_induction.bin_to_nat_pres_incr bin_to_nat_pres_incr cut by (fun (H : cut) b0 => H (bin_to_nat b0)) as patch.
The interface for this is a little tricky; we plan to improve this significantly, since it is a useful way to work around limitations.
PUMPKIN is a research prototype, and so it is currently limited in the kinds of proofs and changes it supports. PUMPKIN is best equipped to handle changes in conclusions of inductive proofs. It has introductory support for changes in hypotheses. It also supports certain changes in definitions (for example, changes in a constructors of an inductive type that a proof inducts over, or changes in a case of a fixpoint that a theorem applies), and some other styles of proofs (for example, simple applicative proofs, or proofs that apply constructors).
With the help of DEVOID, PUMPKIN can also handle certain changes from unindexed types to indexed versions. Please see the DEVOID repository for more of those examples.
PUMPKIN does not yet support adding new hypotheses,
adding constructors to an inductive type, or adding cases to a fixpoint.
PUMPKIN has very limited support for proofs using logic specific to decidable domains
(such as proofs that use omega) and nested induction.
Supporting all of these features is on our roadmap.
For now, if PUMPKIN fails to find a patch, it's likely due to features that are not yet implemented. In any case, if you encounter any error or failure, please cut an issue with a reproducable example, since we can determine whether the error is a bug or an unimplemented feature, and use it as an eventual test case. With that in mind, we are a small research team, so it may take time to implement all of these features. If you would like to contribute directly to the plugin, feel free to cut a pull request.
Right now, there is support for one simple refactoring using the
Replace Convertible command. Just write:
Replace Convertible t in ugly as pretty.
This will replace all subterms of ugly that are convertible to t with t itself,
and define it as a new term pretty.
You can also do this over an entire module Ugly to get a new module Pretty:
Replace Convertible Module t in Ugly as Pretty.
If you'd like, you can also pass in multiple terms to replace (left to right):
Replace Convertible t1 t2 t3 in ugly as pretty.
Replace Convertible Module t1 t2 t3 in Ugly as Pretty.
Work is in progress for a better interface for this, and for commands that do this over multiple files. Please cut an issue if you have any ideas for the ideal interface!
See Replace.v for examples.
One note on this: Even stating what it means for a renaming operation in Coq to be correct requires extremely deep type theory due to the way that equality works, for example over inductive types. This is both cool and sad for users. There is WIP on supporting this.
Proof patching can be used to optimize proofs as well. Optimization removes extra induction
and fixpoints (for fixpoints, you need to run Preprocess first). You can run this command
by running:
Optimize Proof Term slow as fast.
There are some examples of this here. Note that Optimize Proof Term is implemented
on top of Patch Proof, and so will face the same limitations.
The core of PUMPKIN is a set of five core components. We expose four of those components as commands:
Invert trm as id: giventrm : ... -> T1 -> T2, search for an inverse termid : ... -> T2 -> T1Specialize (fun args => f args) as id): applyftoargs, reduce the result, and define this asidAbstract trm to typ as id: abstracttrmto a termid : typFactor trm using prefix id: giventrm : T1 -> Tn, search for factorsid_1: T1 -> T2, ... ,id_n-1: Tn-1 -> Tn
There is also an experimental theorem patching command:
Patch Theorem oldT1 newT1 oldT2 as newT2.
This essentially does dependent substitution of oldT1 with newT1 inside of oldT2, then defines the result as newT2.
Support for this is very preliminary. You can find some examples here.
There are some example proofs to help you get started using PUMPKIN.
You can find these in the coq directory.
You can load them using coqc, coqtop, or your favorite IDE.
The relevant examples are as follows:
- Example.v and Regress.v: Simple changes in conclusions of inductive proofs
- Reverse.v: Isomorphic changes in conclusions of inductive proofs
- Cex.v: Example of the proof from Section 3 of the paper for which the footnote does not hold
- IntegersOld.v and IntegersNew.v: Case study from Section 4.1 of the paper
- Inductive.v: Case study from Section 4.2 of the paper
- divide.v: Case study from Section 4.3 of the paper
- Variants.v: Patch Generation Suite from Section 6 of the paper
- Abstract.v: Example of using the abstraction command
- Theorem.v: Example fo the experimental theorem patching command
- Hypotheses.v: Very simple changes in hypotheses.
We welcome contributors! Especially those willing to help us with build tools, continuous integration, updating Coq versions, documentation, and other infrastructure.
In addition, we have included some useful infrastructure for plugin developers more broadly.
If you've never written a Coq plugin before, you might want to check out the plugin tutorials in the main Coq repository.
To get an idea of how the code is structured, I highly recommend reading Section 5 of the paper and following along in the code. The entry-point to the code is patcher.ml4. You can add new commands there. You can also extend the patch finding procedure or see what it calls out to and modify that. There is a useful debugging function in differencing.ml; if you are modifying the tool, you may want to use it.
Minor note: .ml4 files don't appear to work with a lot of emacs OCaml plugins. You can run tuareg-mode manually on .ml4 files.
This plugin suite includes two useful tools for plugin developers:
- The fix-to-elim plugin for translating fixpoints to inductive proofs
- The coq-plugin-lib library for plugin development
This plugin is maintained by Talia Ringer with help from Nate Yazdani and RanDair Porter. John Leo and Dan Grossman have made conceptual contributions.
The following community members have also contributed to the code:
- Emilio Jesús Gallego Arias
- Your name here!
We use the MIT license because we think that Coq plugins are allowed to do so. If this is incorrect, please let us know kindly so we can fix it.