Also, there seems to be some inefficiency: the posted formula gets proved
quite quickly in HOL4:
Count.apply ARITH_CONV tm;
runtime: 1.2s, gctime: 0.77200s, systime: 0.00000s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 493764; Total: 493764
val it =
⊢ 193650890589077504 * (2 * y + 1) ≤
47942158315484610560 * (2 * x + 1) + 135203236847161865141 ∧
0 ≤
2655641718416121605914624 * (2 * x + 1) +
2208414543647439060992 * (2 * y + 1) + 6004289407548407186399935 ⇒
0 ≤
13137886070707932161376256 * (2 * x + 1) +
17509226798704706453504 * (x + y + 1) + 36152178747194683600721967 ⇔ T:
thm
On Thu, Jan 28, 2021 at 6:57 PM Konrad Slind <konrad.sl...@gmail.com> wrote:
> HOL4 has a notion of persistent theory, so you could spawn many
> parallel sessions, each delivering a theory with one result, then
> create a single descendant theory, import all the parent
> theories, and chain your implications or inequalities there.
>
> It also provides integer decision procedures, so the calls to
> INT_ARITH might possibly be directly substitute-able.
>
> Konrad.
>
>
> On Thu, Jan 28, 2021 at 5:07 PM D. J. Bernstein <d...@math.uic.edu> wrote:
>
>> Thanks for the references and suggestions. As a scaled-down example of
>> part of the time consumption, this takes 400 million CPU cycles:
>>
>> INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1)
>> <= &47942158315484610560 * (&2 * (x:int) + &1)
>> + &135203236847161865141
>> /\
>> &0 <= &2655641718416121605914624 * (&2 * x + &1)
>> + &2208414543647439060992 * (&2 * y + &1)
>> + &6004289407548407186399935
>> ==>
>> &0 <= &13137886070707932161376256 * (&2 * x + &1)
>> + &17509226798704706453504 * (x + y + &1)
>> + &36152178747194683600721967`;;
>>
>> Hand proof: take 6532449000950803555513091/700376017867732114912 and
>> 26794012414555294513937/5603008142941856919296 times the first and
>> second inequalities, add, and observe that you now have a stronger
>> version of the conclusion, offset by 1581608968911709059178093879/256.
>>
>> Changing INT_ARITH to g still takes around 100 million CPU cycles, which
>> makes me wonder whether there's some bottleneck in parsing or printing.
>>
>> The code that I wrote to do a bunch of searching to find and print the
>> whole sequence of relevant presumed theorems is, with no optimization
>> effort, thousands of times faster than this. Of course that code doesn't
>> have to bother with the symbolic aspects of proof manipulation.
>>
>> ---Dan
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
