<div dir="ltr">Hi again.<div><br></div><div>There are over 2200 thms in the hol <a href="http://database.ml">database.ml</a> but there are "to the most"[1] 1885 thms. So where are the rest?</div><div><br></div><div>[1]I tried to load the files commented out in <a href="http://hol.ml">hol.ml</a>.</div><div> </div></div><div class="gmail_extra"><br><div class="gmail_quote">On 25 June 2015 at 12: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">Hi Joe,<div><br></div><div>So I tested the HOL "theorems" also, Here are the results:</div><div><div># List.length(!theorems);;</div><span class=""><div>val it : int = 1670</div></span></div><div><br></div><div>So that means there are 1670 - 1214 = 456 theorems not exported to Opentheory?</div><div><br></div><div><br></div><div><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 25 June 2015 at 12:06, 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"><div>Hi Joe, </div><div><br></div><div>Thanks for the reply.</div><div><br></div>2) So maybe I can try to export them? Cos the more thms I get is better for my tests.<div>but I got more thms when I do this search. Why is that (So far we should have 1214 right? 1214 are those only exported but 1670 are all of them (so far))?</div><div><br></div><div> # List.length (search [])<br></div><div>  ;;</div><div>val it : int = 1670</div><div><br></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 24 June 2015 at 23:11, 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>
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>
<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>
<div><div><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 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 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 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 \"Data.Stream.stream\"".<br>
> # let p = load_proofs<br>
> "/home/robert/Project/laholide/opentheory/natural-prime.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article /home/robert/Project/laholide/opentheory/natural-prime.art at<br>
> line 191: const\nstack = [\"Number.Natural.divides\"; Term; Var; Term; Term;<br>
> Var; \"Number.Natural.prime\"; Term; Var; [[]; [[Var; Term]]]; 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 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 /home/robert/Project/laholide/opentheory/natural-divides.art at<br>
> line 159: defineConst\nstack = [Term; \"Number.Natural.divides\"; Var; 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 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>; Const<!>]\nunknown<br>
> constant \"Number.Modular.modulus\"".<br>
> # let p = load_proofs "/home/robert/Project/laholide/opentheory/gfp.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article /home/robert/Project/laholide/opentheory/gfp.art at line 54:<br>
> const\nstack = [\"Number.GF(p).oddprime\"; Term; Var; []]\nunknown 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 /home/robert/Project/laholide/opentheory/natural-fibonacci.art<br>
> at line 1933: defineConstList\nstack = [Thm;<br>
> [[\"Number.Natural.Fibonacci.zeckendorf\"; Var]]; Var; []; Thm]\nunknown<br>
> constant \"Number.Natural.Fibonacci.zeckendorf\"".<br>
> # let p = load_proofs "/home/robert/Project/laholide/opentheory/word.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article /home/robert/Project/laholide/opentheory/word.art at line 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 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>
</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><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>