Email Gateway (Aug 22 2022 at 10:55): Email Gateway (Aug 22 2022 at 10:55):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear all:
Here I want to ask a question on Isablle's efficiecy and capacity.
My proof is a typical case analysis, whose framework is as follows:
have "case1 \or case2 \or ....\or casen" by auto
moreover
{assume "case1"
proof_1
have "?P"
}
......
moreover
{assume "casen"
proof_n
have "?P"
}
ultimately show “？P"
For each i, proof_i need do case analysis on another variable which contains m-case.
There are two -level of case analyis.
Logically, the proof is simple, just an application of lemma prepared.
However n is 52, which is lager to human, but not to Isabelle, I think.
m is about 13.
Totally there are 52*13 cases.
However the speed to run the proof script is not so quick as I expected, which needs about 26mins. More awfully, the system is slow, and about 1 G memory is needed by Isabelle to
run the proof script.
Interesting people can download the script from http://lcs.ios.ac.cn/~lyj238/question/duan.zip if the attached file is removed by the mail-list server.
Here I want to ask:
whether my proof style for the case analysis is wirteln in a way, which is executed ineffieciently by Isabelle?
if thus, what is the effiect way to write the case analysis proof. Are there some tips to improve the efficieny of Isabelle to prove?
If there is not a problem of my case analysis proof, can Isabelle be more quick and have larger capacity. When n=132, and n=30 in another experiment, Isabelle is stuck.
By the way, all my proof is generated by a generator, and Isabelle is used as a back-end. Therefore you just use the isabelle build way (see the ROOT file).
regards
Email Gateway (Aug 22 2022 at 10:56):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear all:
Here I want to ask a question on Isablle's efficiecy and capacity.
My proof is a typical case analysis, whose framework is as follows:
have "case1 \or case2 \or ....\or casen" by auto
moreover
{assume "case1"
proof_1
have "?P"
}
......
moreover
{assume "casen"
proof_n
have "?P"
}
ultimately show “？P"
For each i, proof_i need do case analysis on another variable which contains m-case.
There are two -level of case analyis.
Logically, the proof is simple, just an application of lemma prepared.
However n is 52, which is lager to human, but not to Isabelle, I think.
m is about 13.
Totally there are 52*13 cases.
However the speed to run the proof script is not so quick as I expected, which needs about 26mins. More awfully, the system is slow, and about 1 G memory is needed by Isabelle to
run the proof script.
Interesting people can download the script from http://lcs.ios.ac.cn/~lyj238/question/duan.zip if the attached file is removed by the mail-list server.
Here I want to ask:
whether my proof style for the case analysis is wirteln in a way, which is executed ineffieciently by Isabelle?
if thus, what is the effiect way to write the case analysis proof. Are there some tips to improve the efficieny of Isabelle to prove?
If there is not a problem of my case analysis proof, can Isabelle be more quick and have larger capacity. When n=132, and n=30 in another experiment, Isabelle is stuck.
By the way, all my proof is generated by a generator, and Isabelle is used as a back-end. Therefore you just use the isabelle build way (see the ROOT file).
regards
Email Gateway (Aug 22 2022 at 10:56):From: Larry Paulson <lp15@cam.ac.uk>
Theorem proving is computational demanding, and in the short term, we have to work around this. If Isabelle proves 676 subgoals in 26 minutes, that’s 2.3 seconds per subgoal. It might be possible to prove your subgoals much faster than this. Use the Timing panel to identify slow steps. I noticed that you call “auto” in many places where “blast” also solves the subgoal, much faster. Look for ways to solve your problem differently.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:56):From: Larry Paulson <lp15@cam.ac.uk>
Theorem proving is computational demanding, and in the short term, we have to work around this. If Isabelle proves 676 subgoals in 26 minutes, that’s 2.3 seconds per subgoal. It might be possible to prove your subgoals much faster than this. Use the Timing panel to identify slow steps. I noticed that you call “auto” in many places where “blast” also solves the subgoal, much faster. Look for ways to solve your problem differently.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC