HOL
HOL copied to clipboard
HOL-Theorem-Prover
proved theorem cache
Similar to #488 but less extreme: Could we have a cache of theorems that have been proved before so that when this option is turned on any attempts to prove the same theorem statement via prove or store_thm is short-circuited (similar to how Holmake --fast works).
I assume this would be intended to benefit interactive sessions. It seems like it would be pretty easy to store every theorem statement in a term-net that could be consulted by store_thm and prove.
The same cache could be consulted after every invocation of e so that the system could tell the user that their goal looked like a known theorem. (This second use-case is harder though because goals will have assumptions and you have to figure out how to canonicalise them against theorem statements that will also have assumptions. I guess you match on conclusions and then look for subsets over assumptions after canonicalising.)
In addition, the use of term-nets would make it easy to allow instances of (implicitly or not) universally quantified theorems to prove goals.
Although it would be good just for interactive sessions, I'm also interested in a cache that persists between process invocations. The situation I'm trying to speed up is fixing/tweaking proofs near the end of a long-running script, where the fixes have to do with global context (like grammar or what theories are open) -- maybe such work is intrinsically slow...
There is a possible problem that proofs for the same sequent are not interchangeable in the general case because of tags. In most practical cases, this is probably no obstacle, but a method should be provided to force evaluation of the tactic.
I was thinking that this cache would be off by default and only turned on in special circumstances (like when repeatedly trying to fix a proof at the end of a long-running script). (If it can be made safe and robust for general use, all the better.)
@xrchz Can you please provide an example proof that would benefit from a ((goal,tactic (string)),(input,output)) cache?
Encapsulating e with a recorder and replayer seems the least invasive way of doing it. The problem from my point of view is to find a way to store the tactic so that you can check for equality.
I am not sure I understand the problem correctly. If the effect of the long-lasting tactic is known, why not just replace it by a tactic that maps its input to its output since it isn't modified by your global context?