Re: [isabelle] Extreme processing time for function definition

Note that up to the point where pat_completeness generates 46057 subgoals, things are not so bad. Proving all those (simple!) subgoals is the killer.


On 08/07/2021 10:10, Manuel Eberl wrote:
Hmm, I wonder if some of the non-mandatory features of the function
package (such as the generation of elimination rules) might affect the
performance negatively here. Perhaps one could try to put an option into
the function package to disable the generation of these and see what

(Full disclosure: I wrote the code that generates the pelims/elims rules
back in the day, so if this is the issue, it's my fault. :D )


On 08/07/2021 03:28, Eugene W. Stark wrote:
Thanks!  The ideas for reducing the processing time are very helpful.

I think there is something else going on besides the sheer number of subgoals, because removing
the last four clauses in my original example still leaves about 18,000 subgoals, but the processing
time is only about 3 minutes.  I guess when the patterns are expanded to the next level of depth
it applies a multiplicative factor to the time taken to discharge the subgoals.  One gets used to
the function package often working so well that it is quite startling to see an exponential jump in
processing time with relatively small changes to the definitions.

Right now I am confused, though, and I have to go back and re-do my homework on this definition.
I hit a blocking point in the series of lemmas I was trying to generalize and I jumped to the conclusion
that I had missed some critical pairs (hence the additional four clauses), but at this moment I am not
so sure any more.

Anyway, your ideas at least provide me with some control over my fate.  Thanks again!

On 7/7/21 4:02 PM, Tobias Nipkow wrote:
Attached you find a version that works in reasonable time. I reduced the size of the patterns by replacing all "Var 0"
by "vn" and testing if "vn ~= Var 0 \/ ...". This got the number of cases just below 10.000. [I believe I did not change
the meaning of the equations as a result]

Note that the problem of minimizing the number of cases is hard:


On 07/07/2021 16:51, Eugene W. Stark wrote:
The 45-line definition of function "resid" in the attached theory takes between 30 and 40 minutes
to process.  This time increased very rapidly from a previous value of about 3 minutes when I added
four clauses (the four preceding the final default clause).  The original definition was stated with
"fun" but I split it up using "function" to try to see which part was consuming the time.
About one minute is used to process the "function (sequential)" declaration, with the remainder of
the time going to the proof of 46057 subgoals "by pat_completeness auto".  The termination proof
does not take significant time.  I note that the time-consuming portion appears to be single-threaded.

Is there anything I can do, or am I out of luck?  The 30-40 minute processing time is probably
prohibitive for what I was trying to do, so it looks like I will have to abandon the generalization
I was trying to make and revert to a simpler version that processes in reasonable time.

Thanks for any suggestions.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.