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
