When I try it in HOL Light on my machine it takes about 0.074 seconds, which is around 250 million CPU cycles according to the clock speed from "lscpu". This is the same order of magnitude that Dan was seeing.
On the whole, the procedures like INT_ARITH are mostly fast enough for everyday interactive proofs, but may not be suited for cases where efficiency really matters. There are certain fundamental limitations on how fast one can get, subject to the need to produce a formal proof (particularly given that HOL Light requires arithmetic calculation to be done by inference). Nevertheless one can usually do a lot better than the everyday tactics, with a bit of effort. One place to look would be the work Alexey Solovyev did for the Flyspeck inequalities, which is in the HOL Light directory: Formal_ineqs/ That is often capable of proving large real linear inequalities amazingly quickly. But there may also be some more specific optimizations that would apply to Dan's problems or might suit them better, particularly if it is "small easy inequalities solved huge numbers of times". And yes, parsing and typechecking is usually even slower, so you would definitely want to avoid that in the inner loop if possible. John. On Thu, Jan 28, 2021 at 5:05 PM Konrad Slind <konrad.sl...@gmail.com> wrote: > Just for clarification: the HOL4 term parser handled the supplied term > without alteration, and > intLib.ARITH_CONV is the HOL4 analog of INT_ARITH. > > > > > On Thu, Jan 28, 2021 at 6:59 PM Konrad Slind <konrad.sl...@gmail.com> > wrote: > >> 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 >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
