Email Gateway (Aug 18 2022 at 13:10): Email Gateway (Aug 18 2022 at 13:10):From: Dennis Walter <dennis.walter@gmail.com>
Hi all,
I'm having problems solving large structured goals involving many
parameters. Even rule applications like
apply (rule allI | rule impI | erule conjE)+
take several minutes. I've experienced this slowdown in cases where
the number of parameters (bound meta-variables) is > 30, and these
repeatedly occur in various places within the goal (~2000 lines, no
abbreviations). I suspect that Isabelle's lifting of rules over
parameters is to blame, but I can't see why this should be the case.
Can anybody explain this phenomenon to me?
Thanks a lot,
Dennis
Email Gateway (Aug 18 2022 at 13:10):From: Lawrence Paulson <lp15@cam.ac.uk>
It looks like you are working on rather large problems! Still I don't
think such runtimes should be normal. Are you using Poly/ML? Does your
machine have ample memory?
Larry Paulson
Email Gateway (Aug 18 2022 at 13:10):From: Makarius <makarius@sketis.net>
Incidently, I've come across a similar situation just 2 weeks ago, with
approx. 10 parameters and 10 premises in the goal, but the same numbers in
the rule being applied. It took several minutes to apply the rules.
Can you produce a selfcontained example of your application, so that we
can get check if this is really the same hot spot?
Makarius
Email Gateway (Aug 18 2022 at 13:11):From: Dennis Walter <dennis.walter@gmail.com>
I tried to, but failed in the amount of time I've got right now. The
concrete problem is a little too large (and dependent on other
theories) to show here.
The structure of the subgoal is sth like this:
! n1 n2 n3 n4 n5 n6 n7 n8 n9.
[| P1 n1 ... n9 & P2 n2 ... n9 & P3 n3 ... n9 & ...|] ==>
ALL S. f S' = S -->
(ALL S1. f S = S1 -->
(ALL S2. f S2 = S1 -->
(... -->
(let v = g S in
ALL S'. f S = S' -->
(let v = g S' in
ALL S. f S' = S -->
...
in P n1 n2 n3 n4 n5 n6 n7 n8 n9)...)
where the P_i aren't just constants / free variables, but complex
terms referring to the n_i. When I do "apply (rule allI, rule impI,
erule conjE)" with about 30 possible rule applications, it takes
around one minute.
I'll try to come up with a concrete example later.
Dennis
Email Gateway (Aug 18 2022 at 13:12):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Lawrence Paulson wrote:
I can't find the notation '+' in the Isar reference, but I'm guessing
that what you're doing is the equivalent of
REPEAT (rtac allI 1 ORELSE rtac impI 1 ORELSE etac conjE 1)
(or perhaps REPEAT1)
so try instead
REPEAT_DETERM (rtac allI 1 ORELSE rtac impI 1 ORELSE etac conjE 1)
I've found in the past that this sort of change makes a difference. The
reason (I guessed) is that although both versions do, in a sense, the
same amount of useful work for you up to the point where you get the
first new goal-state, the REPEAT version creates and saves all sorts of
data structures which enable backtracking, whereas in the REPEAT_DETERM
version, these get thrown away (REPEAT_DETERM will not allow backtracking).
Jeremy
Last updated: May 03 2024 at 04:19 UTC