<div dir="ltr"><div>Dear Joe,</div><div><br></div>I tried to update the <a href="http://arith.ml">arith.ml</a> file. It seems more complicated than I expected. <div>For example, we have LE_ZERO but the new version deleted it.</div><div><br></div><div>So shall I continue or maybe you have better advice?</div><div>Regards,</div><div>Robert</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 29 June 2015 at 19:16, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Dear Joe,<div>I think HOL Light is more updated. We maybe need to export some files again. </div><div>For example. the <a href="http://arith.ml" target="_blank">arith.ml</a></div><div>The first missing thm is ADD_SUBR, while in the up-to-date HOL Light they have ADD_SUBR defined but not in OpenTheory HOL. </div><div>So I have the feeling that we need to generate the base.art again I think?</div><div><br></div><div>Regards,</div><div>Robert</div><div><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 26 June 2015 at 06:44, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert,<br> <br> This is a mystery to me: perhaps there are many theorems deleted in<br> the OpenTheory fork of HOL Light compared to the standard distribution<br> (which is what the <a href="http://database.ml" rel="noreferrer" target="_blank">database.ml</a> file records)?<br> <br> Cheers,<br> <br> Joe<br> <br> <br> On Thu, Jun 25, 2015 at 3:26 AM, Robert White<br> <div><div><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>> wrote:<br> > Hi again.<br> ><br> > There are over 2200 thms in the hol <a href="http://database.ml" rel="noreferrer" target="_blank">database.ml</a> but there are "to the<br> > most"[1] 1885 thms. So where are the rest?<br> ><br> > [1]I tried to load the files commented out in <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>.<br> ><br> ><br> > On 25 June 2015 at 12:16, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>><br> > wrote:<br> >><br> >> Hi Joe,<br> >><br> >> So I tested the HOL "theorems" also, Here are the results:<br> >> # List.length(!theorems);;<br> >> val it : int = 1670<br> >><br> >> So that means there are 1670 - 1214 = 456 theorems not exported to<br> >> Opentheory?<br> >><br> >><br> >><br> >><br> >> On 25 June 2015 at 12:06, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>><br> >> wrote:<br> >>><br> >>> Hi Joe,<br> >>><br> >>> Thanks for the reply.<br> >>><br> >>> 2) So maybe I can try to export them? Cos the more thms I get is better<br> >>> for my tests.<br> >>> but I got more thms when I do this search. Why is that (So far we should<br> >>> have 1214 right? 1214 are those only exported but 1670 are all of them (so<br> >>> far))?<br> >>><br> >>> # List.length (search [])<br> >>> ;;<br> >>> val it : int = 1670<br> >>><br> >>><br> >>> On 24 June 2015 at 23:11, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:<br> >>>><br> >>>> Hi Robert,<br> >>>><br> >>>> Welcome back!<br> >>>><br> >>>> 1) There hasn't been much development on OpenTheory in recent weeks,<br> >>>> just some extensions to the natural-divides theory to support my<br> >>>> recent blog post on the extended GCD algorithm:<br> >>>><br> >>>><br> >>>> <a href="https://gilith.wordpress.com/2015/06/24/natural-number-greatest-common-divisor/" rel="noreferrer" target="_blank">https://gilith.wordpress.com/2015/06/24/natural-number-greatest-common-divisor/</a><br> >>>><br> >>>> 2) There is no real reason why those HOL Light theories have not been<br> >>>> ported to OpenTheory, except that some of them might not be needed to<br> >>>> compile a standard theory library (which is a common base of theories<br> >>>> that is expected to be implemented in every theorem prover).<br> >>>><br> >>>> We do not use the <a href="http://database.ml" rel="noreferrer" target="_blank">database.ml</a> file which lists all the theorems in the<br> >>>> main branch of the HOL Light theorem prover (not the OpenTheory fork).<br> >>>> But I've just checked in a version of the fork that creates a theorem<br> >>>> database of the standard theory library at the bottom of the <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a><br> >>>> file, so after loading with #use "<a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>";; you can search the<br> >>>> database like so:<br> >>>><br> >>>> # search [`MAX (SUC m) (SUC n)`];;<br> >>>> val it : (string * thm) list =<br> >>>> [("MAX_SUC", |- !m n. MAX (SUC m) (SUC n) = SUC (MAX m n))]<br> >>>><br> >>>> 3) It looks like you need to extend_the_interpretation before loading<br> >>>> the proofs as described in<br> >>>><br> >>>> <a href="http://www.gilith.com/opentheory/mailing-list/2015-June/000515.html" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list/2015-June/000515.html</a><br> >>>><br> >>>> Cheers,<br> >>>><br> >>>> Joe<br> >>>><br> >>>> On Wed, Jun 24, 2015 at 1:31 PM, Robert White<br> >>>> <<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>> wrote:<br> >>>> > Dear Joe and all,<br> >>>> ><br> >>>> > I am back to the community!<br> >>>> ><br> >>>> > I have the following questions and updates for you:<br> >>>> ><br> >>>> > 1) I will be finishing my internship in a few weeks and it would be<br> >>>> > nice of<br> >>>> > you if you can give me some description of the most recent updates of<br> >>>> > OpenTheory.<br> >>>> ><br> >>>> > 2)<br> >>>> > I noticed there is a part not imported to Opentheory (in <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>) :<br> >>>> ><br> >>>> > (* Not yet ported to OpenTheory<br> >>>> > loads "<a href="http://calc_int.ml" rel="noreferrer" target="_blank">calc_int.ml</a>";; (* Calculation with integer-valued reals<br> >>>> > *)<br> >>>> > loads "<a href="http://realarith.ml" rel="noreferrer" target="_blank">realarith.ml</a>";; (* Universal linear real decision procedure<br> >>>> > *)<br> >>>> > loads "<a href="http://real.ml" rel="noreferrer" target="_blank">real.ml</a>";; (* Derived properties of reals<br> >>>> > *)<br> >>>> > loads "<a href="http://calc_rat.ml" rel="noreferrer" target="_blank">calc_rat.ml</a>";; (* Calculation with rational-valued reals<br> >>>> > *)<br> >>>> > loads "<a href="http://int.ml" rel="noreferrer" target="_blank">int.ml</a>";; (* Definition of integers<br> >>>> > *)<br> >>>> > loads "<a href="http://iterate.ml" rel="noreferrer" target="_blank">iterate.ml</a>";; (* Iterated operations<br> >>>> > *)<br> >>>> > loads "<a href="http://cart.ml" rel="noreferrer" target="_blank">cart.ml</a>";; (* Finite Cartesian products<br> >>>> > *)<br> >>>> > *)<br> >>>> ><br> >>>> > Is there any reason why not?<br> >>>> ><br> >>>> > Also, there is a <a href="http://database.ml" rel="noreferrer" target="_blank">database.ml</a> file. Shall I ignore that in OpenTheory<br> >>>> > HOL?<br> >>>> > (since it is not complete anyway)<br> >>>> ><br> >>>> > 3)<br> >>>> > I have problem loading article files:<br> >>>> ><br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/stream.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article /home/robert/Project/laholide/opentheory/stream.art at<br> >>>> > line<br> >>>> > 1273: defineTypeOp\nstack = [Thm; [\"A\"]; \"Data.Stream.nth\";<br> >>>> > \"Data.Stream.fromFunction\"; \"Data.Stream.stream\"; Var; Var;<br> >>>> > \"Data.Stream.unfold\"; Var; \"Data.Stream.iterate\";<br> >>>> > \"Data.Stream.replicate\"]\nunknown type operator<br> >>>> > \"Data.Stream.stream\"".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/natural-prime.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article<br> >>>> > /home/robert/Project/laholide/opentheory/natural-prime.art at<br> >>>> > line 191: const\nstack = [\"Number.Natural.divides\"; Term; Var; Term;<br> >>>> > Term;<br> >>>> > Var; \"Number.Natural.prime\"; Term; Var; [[]; [[Var; Term]]];<br> >>>> > Thm]\nunknown<br> >>>> > constant \"Number.Natural.divides\"".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/natural-divide.art";;<br> >>>> > Exception:<br> >>>> > Sys_error<br> >>>> > "/home/robert/Project/laholide/opentheory/natural-divide.art: No such<br> >>>> > file<br> >>>> > or directory".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/natural-divides.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article<br> >>>> > /home/robert/Project/laholide/opentheory/natural-divides.art at<br> >>>> > line 159: defineConst\nstack = [Term; \"Number.Natural.divides\"; Var;<br> >>>> > Var;<br> >>>> > []]\nunknown constant \"Number.Natural.divides\"".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/modular.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article /home/robert/Project/laholide/opentheory/modular.art at<br> >>>> > line<br> >>>> > 155: const\nstack = [\"Number.Modular.modulus\"; Term; Term; Var; Var;<br> >>>> > \"Number.Modular.equivalent\"; Term; Var; Term; Var; [];<br> >>>> > \"HOLLight.modular_to_class\"; \"HOLLight.modular_from_class\";<br> >>>> > \"Number.Modular.modular\"; TypeOp<fun>; TypeOp<fun>;<br> >>>> > Const<!>]\nunknown<br> >>>> > constant \"Number.Modular.modulus\"".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/gfp.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article /home/robert/Project/laholide/opentheory/gfp.art at line<br> >>>> > 54:<br> >>>> > const\nstack = [\"Number.GF(p).oddprime\"; Term; Var; []]\nunknown<br> >>>> > constant<br> >>>> > \"Number.GF(p).oddprime\"".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/natural-fibonacci.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article<br> >>>> > /home/robert/Project/laholide/opentheory/natural-fibonacci.art<br> >>>> > at line 1933: defineConstList\nstack = [Thm;<br> >>>> > [[\"Number.Natural.Fibonacci.zeckendorf\"; Var]]; Var; [];<br> >>>> > Thm]\nunknown<br> >>>> > constant \"Number.Natural.Fibonacci.zeckendorf\"".<br> >>>> > # let p = load_proofs<br> >>>> > "/home/robert/Project/laholide/opentheory/word.art";;<br> >>>> > Exception:<br> >>>> > Failure<br> >>>> > "in article /home/robert/Project/laholide/opentheory/word.art at line<br> >>>> > 130:<br> >>>> > const\nstack = [\"Data.Word.width\"; Term; \"Data.Word.modulus\"; Thm;<br> >>>> > Thm]\nunknown constant \"Data.Word.width\"".<br> >>>> > #<br> >>>> ><br> >>>> > Could you please help on that? It seems I can't even play with the<br> >>>> > other<br> >>>> > article files I used to be able to load either :(<br> >>>> ><br> >>>> > Thanks very much!<br> >>>> ><br> >>>> > --<br> >>>> ><br> >>>> > Regards,<br> >>>> > Robert White (Shuai Wang)<br> >>>> > INRIA Deducteam<br> >>>> > [Moving to ILLC of UvA from this Sep to continue my masters. ]<br> >>>> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]<br> >>>> ><br> >>><br> >>><br> >>><br> >>><br> >>> --<br> >>><br> >>> Regards,<br> >>> Robert White (Shuai Wang)<br> >>> INRIA Deducteam<br> >>> [Moving to ILLC of UvA from this Sep to continue my masters. ]<br> >>> [New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]<br> >>><br> >><br> >><br> >><br> >> --<br> >><br> >> Regards,<br> >> Robert White (Shuai Wang)<br> >> INRIA Deducteam<br> >> [Moving to ILLC of UvA from this Sep to continue my masters. ]<br> >> [New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]<br> >><br> ><br> ><br> ><br> > --<br> ><br> > Regards,<br> > Robert White (Shuai Wang)<br> > INRIA Deducteam<br> > [Moving to ILLC of UvA from this Sep to continue my masters. ]<br> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]<br> ><br> </div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep <span style="font-size:small">to continue my masters</span><span style="font-size:12.8000001907349px">. ]</span></div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div> </div> </div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep <span style="font-size:small">to continue my masters</span><span style="font-size:12.8000001907349px">. ]</span></div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div> </div>