HOL-Theorem-Prover
Simplifier to produce minimised proof script after it finds it
Sometimes when you call simp (or gvs etc.) it spends a lot of time finding things that can be done but in the end what is actually done is rewriting with only a few rewrites or only in a few places. This issue is about separating proof search from proof replay: after the search, you get something faster and more maintainable to save in your script file.
(Suggestion in HOL workshop from @myreen )
To be honest, I think this will likely produce much less robust proofs that also become textually larger and grosser.
In particular, if you store the details of where to rewrite you are presumably storing assumption numbers coupled with term positions, both of which seem like things that are really likely be fragile.
The plan would only store the list theorems used to simplify . so that you simplify with a pure_simp_tac variant
If I understand correctly, you would thus be replacing simp[..] invocations with something like
simp_tac pure_ss [th1, th2, .. , thn, ASSUME “assumption1“, ASSUME “assumption2”, ... ASSUME “assumptions”, SF ARITH_ss, SF somethingelse]
where th1..n are those theorems actually used from the stateful rewriter, and where assumption1..n are those assumptions actually used. Of course, if you're reworking a gvs call, you will have multiple such (one for each simplified assumption) because gvs simplifies each assumption independently, and using different contexts.
By making the proof script much larger you are definitely not making it more maintainable.
I think someone should be profiling some of the relevant code to see where the slowness is coming from.
I was thinking it would be more simp[] to asm_simp_tac(pure_ss)[..] but i'm not sure whether @myreen or @digama0 thinks the same.
The maintainability comes from that new simp rules won't break old proofs.
If the list of used theorems is small, I can see this being useful, but we would need to profile invocations to see how many get used per invocation to really get a sense for how potent this would be.
My periodic reminder that a crude beginning of such profiling is already in simpLib.trace_rewrites and simpLib.used_rewrites.
