[isabelle-dev] HOL/Number_Theory/Primes

[Peter Lammich]

Is this another application for the new NOMATCH simproc?

--
  Peter


On Fr, 2014-11-07 at 18:34 +0100, Tobias Nipkow wrote:
> 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.haftmann at 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-dev at in.tum.de
> >>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> >>>>>
> >>>> _______________________________________________
> >>>> isabelle-dev mailing list
> >>>> isabelle-dev at in.tum.de
> >>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> >>>
> >>> _______________________________________________
> >>> isabelle-dev mailing list
> >>> isabelle-dev at in.tum.de
> >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> >>
> >>
> >>
> >> _______________________________________________
> >> isabelle-dev mailing list
> >> isabelle-dev at in.tum.de
> >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> >
> >
> >
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> >
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev