proved theorem cache

[xrchz]

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).

[mn200]

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.

[xrchz]

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...

[marioxcc]

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.

[xrchz]

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.)

[barakeel]

@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.

[barakeel]

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?