[isabelle-dev] HOL/Number_Theory/Primes

[Tobias Nipkow]

On 07/11/2014 19:05, Peter Lammich wrote:
> Is this another application for the new NOMATCH simproc?

One could patch this particular problem, but I would be very uneasy with a setup 
that has no clear rewrite ordering between these two functions.

Tobias

> --
>    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
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141107/e6d17827/attachment.bin>