<div dir="ltr">Dear Joe,<div><br></div><div>Thanks for the reply. I am looking forward to the updates!<br><div><br></div><div>Here are things I found which might be useful for you:</div><div><br></div><div>1)</div><div><div>Looks like there is something wrong going on there in <a href="http://sum.ml">sum.ml</a>:<br></div><div>Exception: Failure "REFL_TAC".</div><div>Error in included file ----/hol_light/opentheory/stdlib/<a href="http://sum.ml">sum.ml</a></div></div><div><br></div><div>2) There is no CASES_TAC in the most up-to-date version of HOL Light.</div><div><br></div><div>Questions: </div><div>1) Why do you want things to be different?</div><div><br></div><div>Cheers</div><div>Robert</div><div><br></div><div><br></div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 29 June 2015 at 20:30, 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>
In general there are quite a few differences in definitions and<br>
theorems between the OpenTheory fork of HOL Light and the trunk, and<br>
some of that is here to stay (e.g., the explicit type of sets in the<br>
OpenTheory fork).<br>
<br>
That said, it's past time to do a merge with the HOL Light trunk and<br>
create a new version of the standard theory library: I will work on<br>
this.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<br>
<br>
On Mon, Jun 29, 2015 at 10:43 AM, Robert White<br>
<div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe,<br>
><br>
> I tried to update the <a href="http://arith.ml" rel="noreferrer" target="_blank">arith.ml</a> file. It seems more complicated than I<br>
> expected.<br>
> For example, we have LE_ZERO but the new version deleted it.<br>
><br>
> So shall I continue or maybe you have better advice?<br>
> Regards,<br>
> Robert<br>
><br>
> On 29 June 2015 at 19:16, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>><br>
> wrote:<br>
>><br>
>> Dear Joe,<br>
>> I think HOL Light is more updated. We maybe need to export some files<br>
>> again.<br>
>> For example. the <a href="http://arith.ml" rel="noreferrer" target="_blank">arith.ml</a><br>
>> The first missing thm is ADD_SUBR, while in the up-to-date HOL Light they<br>
>> have ADD_SUBR defined but not in OpenTheory HOL.<br>
>> So I have the feeling that we need to generate the base.art again I think?<br>
>><br>
>> Regards,<br>
>> Robert<br>
>><br>
>><br>
>> On 26 June 2015 at 06:44, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
>>><br>
>>> 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>
>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">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">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">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<br>
>>> >>> better<br>
>>> >>> for my tests.<br>
>>> >>> but I got more thms when I do this search. Why is that (So far we<br>
>>> >>> should<br>
>>> >>> have 1214 right? 1214 are those only exported but 1670 are all of<br>
>>> >>> 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">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>
>>> >>>><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<br>
>>> >>>> been<br>
>>> >>>> ported to OpenTheory, except that some of them might not be needed<br>
>>> >>>> to<br>
>>> >>>> compile a standard theory library (which is a common base of<br>
>>> >>>> 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<br>
>>> >>>> the<br>
>>> >>>> main branch of the HOL Light theorem prover (not the OpenTheory<br>
>>> >>>> fork).<br>
>>> >>>> But I've just checked in a version of the fork that creates a<br>
>>> >>>> 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<br>
>>> >>>> loading<br>
>>> >>>> the proofs as described in<br>
>>> >>>><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">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<br>
>>> >>>> > be<br>
>>> >>>> > nice of<br>
>>> >>>> > you if you can give me some description of the most recent updates<br>
>>> >>>> > 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<br>
>>> >>>> > 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<br>
>>> >>>> > 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<br>
>>> >>>> > 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;<br>
>>> >>>> > 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<br>
>>> >>>> > 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\";<br>
>>> >>>> > 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<br>
>>> >>>> > at<br>
>>> >>>> > line<br>
>>> >>>> > 155: const\nstack = [\"Number.Modular.modulus\"; Term; Term; Var;<br>
>>> >>>> > 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<br>
>>> >>>> > 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<br>
>>> >>>> > line<br>
>>> >>>> > 130:<br>
>>> >>>> > const\nstack = [\"Data.Word.width\"; Term; \"Data.Word.modulus\";<br>
>>> >>>> > 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">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">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">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">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">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">shuai.wang@student.uva.nl</a>]<br>
><br>
</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>