search

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
MIT License
51 stars 2 forks source link

Merge Nate's fixpoint to induction principle translation in from DEVOID (fixes #5) #13

Closed tlringer closed 5 years ago

tlringer commented 5 years ago

This code is almost entirely @nateyazdani's, plus some auxiliary functionality from DEVOID.

This merges in the Preprocess command. See the README for more details. This broadens the proofs that PUMPKIN PATCH can handle.

This does not yet have good evar map hygiene, and it's currently a bit messy. There's not really much use refactoring right now, though, since there will be a major refactor when we merge in the rest of DEVOID (for example, we will likely remove the proofcat representation). The same holds for better evar map and universe hygiene. So I've saved those tasks for later. For now this just preserves the old behavior.

This does not yet run automatically. I also have a separate issue for that.

I've tested this. Nate, I'd like you to do a sanity check to make sure I didn't accidentally butcher your code somewhere. I'm going to give myself a CR later just to check the code, too.

tlringer commented 5 years ago

I did a sanity check and it's fine except for the bad evar hygiene I know about; Nate I still want you to peek tomorrow after I merge just to check for any minor problems in merging, but for the most part I just copied your functions over and the tests still work, so I don't anticipate any issues. Regression tests still pass, too.