Simple rewrite tactic decompilation

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

MIT License

51 stars 2 forks source link

Simple rewrite tactic decompilation #73

Closed randair closed 4 years ago

randair commented 4 years ago

Simple cases:

rewrite H
rewrite <- H
Sequences of the above.
Simplifies eq_ind etc. from eta expanded form

./build.sh && ./test.sh

randair commented 4 years ago

The tests I have were verified by just my eyes. Haven’t decided how I’ll automate them yet. Maybe a decompile command that writes to the console, pipe it to a file and diff it with the correct tactic outputs.

randair commented 4 years ago

Pushed minor bugfix for intros. fun (_ H) => H was compiled to:

intros H H.
apply H.

This was because the second argument wasn't anonymous, so it used its own name despite generating the same name for the first argument. Now gives:

intros H H0.
apply H0.

Putting intros _ doesn't always work because of cases we've seen before where an argument's name might be destructed as "Anonymous" yet somehow still be used in the proof term.