Thanks for finding this out. The theorem is "a dvd b ==> b mod a = 0"
This applies to any term "a mod b" and creates a subgoal "a dvd b". Normally, that is not too bad. But if a and b are numerals, this leads to a loop with the rewrite rule Divides.dvd_eq_mod_eq_0_numeral:
(numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0)The enormous runtimes where due to this loop. It was not an infinite loop because the simplifier has a depth limit.
Clearly, we cannot have such a loop. Either mod can use dvd or the other way around, but not both.
Thanks for simp_trace_new/Lars Hupel, it made it easy to find out what was going on. [It would be nice if the trace could also show when the depth limit is exceeded, it does not seem to].
Tobias On 07/11/2014 17:45, Dmitriy Traytel wrote:
The culprit seems to be dvd_imp_mod_0 introduced as a simp rule in 773b378d9313. The following takes again only 2 seconds. declare dvd_imp_mod_0[simp del] lemma "prime(97::nat)" by simp Dmitriy On 07.11.2014 15:31, Tobias Nipkow wrote:Very nice observations, thank you. I was obviously too hasty to remove the test which exposed this time leak. Once this issue has been fixed, I will put the "long" test back in, with a better comment. Tobias On 07/11/2014 15:27, Dmitriy Traytel wrote:This is in Isabelle2014. In 229765cc3414 I make the same measurements as Larry. So indeed (as the text above those lemmas suggests) there seems to be a regression with the simplifier setup. Dmitriy On 07.11.2014 15:10, Julian Brunner wrote:The proof that 97 is prime only takes 1.3s on my machine (2.7 GHz i7), with the whole theory Primes loading in about 4 seconds. On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> wrote:This theory takes quite a while to load, and I have found out why: text{* A bit of regression testing: *} lemma "prime(97::nat)" by simp lemma "prime(997::nat)" by eval The proof that 97 is prime takes 35 seconds on a very fast machine. Can we get rid of this or at least substitute a smaller number?The question is whether this has really to be performed using simp. As an alternative, a suitable code equations could be proven using the primes_upto in Eratosthenes.thy, but I did never take any measurements at which threshold the additional data structures outperform brute-force calculation. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
