Re: [isabelle] Extreme processing time for function definition



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: https://www21.in.tum.de/~krauss/publication/2008-patterns/
> 
> Tobias
> 
> 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.
>>





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