Re: [isabelle] Extreme processing time for function definition



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

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

Manuel


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

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



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