Email Gateway (Aug 18 2022 at 11:41): Email Gateway (Aug 18 2022 at 11:41):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
Hello there.
I've been using Isabelle for some while, and have become a tad frustrated
with the amount of time which is spent re-running proof scripts as I move
from file to file. Many of these proofs have been unchanged in my
repository for years now, and have presumably been re-executed thousands
of times.
The idea is to use the proof-recording mechanism to get a list of
dependencies when a theorem is proved, which goes in to some kind of
cache. When a theorem is stated, we can check whether it hits anything in
the cache, and if so, whether the assumptions exist in the current context
and match term-for-term. If all of this is true, we can skip the proof,
since it would probably have succeeded anyway. It's not perfect, and you'd
certainly have to do regression tests regularly, but it could make a big
difference to the cost of manipulating a large proof repository.
The checks seem fairly straightforward, but I'm stuck on hooking this
thing into Isar. It's fairly clear that the hook for skipping the proof
should be in begin_proof in toplevel.ML, where skip_proofs is checked
already. The information available at this point (in a Proof.state) does
not, however, tell us exactly what the final theorem will look like.
Instead we have an intermediate theorem and a list of assumptions.
One option was to work entirely in terms of the intermediate theorem,
giving us a good match for our skip hook. However, in a proof that ends
"by auto", the final Proof.state, the one manipulated by end_proof, is the
one that existed before auto was run, and doesn't have a complete list of
dependencies.
The next step down the abstraction chain seems to be to try to work with a
Context.proof, at which point the just-proved theorem seems to become
anonymous, and I get totally lost.
Does anyone have a sensible idea for where to put the hook for trapping
completed theorems? Additionally, if this is done after the theorem is
converted from its intermediate to its final form, is there an easy way to
check one against the other? (This may be a related question, since one
thing we can certainly do when deciding whether to skip is to skip and
complete the proof, and see what gets caught at our hooks).
I appreciate that this may not be possible, and will be interested in the
discussion regardless.
Yours,
Thomas.
Last updated: May 03 2024 at 04:19 UTC