[opentheory-users] error loading article files (again?).

[Joe Leslie-Hurd]

Hi Robert,

Welcome back!

1) There hasn't been much development on OpenTheory in recent weeks,
just some extensions to the natural-divides theory to support my
recent blog post on the extended GCD algorithm:

https://gilith.wordpress.com/2015/06/24/natural-number-greatest-common-divisor/

2) There is no real reason why those HOL Light theories have not been
ported to OpenTheory, except that some of them might not be needed to
compile a standard theory library (which is a common base of theories
that is expected to be implemented in every theorem prover).

We do not use the database.ml file which lists all the theorems in the
main branch of the HOL Light theorem prover (not the OpenTheory fork).
But I've just checked in a version of the fork that creates a theorem
database of the standard theory library at the bottom of the hol.ml
file, so after loading with #use "hol.ml";; you can search the
database like so:

# search [`MAX (SUC m) (SUC n)`];;
val it : (string * thm) list =
  [("MAX_SUC", |- !m n. MAX (SUC m) (SUC n) = SUC (MAX m n))]

3) It looks like you need to extend_the_interpretation before loading
the proofs as described in

http://www.gilith.com/opentheory/mailing-list/2015-June/000515.html

Cheers,

Joe

On Wed, Jun 24, 2015 at 1:31 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe and all,
>
> I am back to the community!
>
> I have the following questions and updates for you:
>
> 1) I will be finishing my internship in a few weeks and it would be nice of
> you if you can give me some description of the most recent updates of
> OpenTheory.
>
> 2)
> I noticed there is a part not imported to Opentheory (in hol.ml) :
>
> (* Not yet ported to OpenTheory
> loads "calc_int.ml";;   (* Calculation with integer-valued reals
> *)
> loads "realarith.ml";;  (* Universal linear real decision procedure
> *)
> loads "real.ml";;       (* Derived properties of reals
> *)
> loads "calc_rat.ml";;   (* Calculation with rational-valued reals
> *)
> loads "int.ml";;        (* Definition of integers
> *)
> loads "iterate.ml";;    (* Iterated operations
> *)
> loads "cart.ml";;       (* Finite Cartesian products
> *)
> *)
>
> Is there any reason why not?
>
> Also, there is a database.ml file. Shall I ignore that in OpenTheory HOL?
> (since it is not complete anyway)
>
> 3)
> I have problem loading article files:
>
> # let p = load_proofs
> "/home/robert/Project/laholide/opentheory/stream.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/stream.art at line
> 1273: defineTypeOp\nstack = [Thm; [\"A\"]; \"Data.Stream.nth\";
> \"Data.Stream.fromFunction\"; \"Data.Stream.stream\"; Var; Var;
> \"Data.Stream.unfold\"; Var; \"Data.Stream.iterate\";
> \"Data.Stream.replicate\"]\nunknown type operator \"Data.Stream.stream\"".
> # let p = load_proofs
> "/home/robert/Project/laholide/opentheory/natural-prime.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/natural-prime.art at
> line 191: const\nstack = [\"Number.Natural.divides\"; Term; Var; Term; Term;
> Var; \"Number.Natural.prime\"; Term; Var; [[]; [[Var; Term]]]; Thm]\nunknown
> constant \"Number.Natural.divides\"".
> # let p = load_proofs
> "/home/robert/Project/laholide/opentheory/natural-divide.art";;
> Exception:
> Sys_error
>  "/home/robert/Project/laholide/opentheory/natural-divide.art: No such file
> or directory".
> # let p = load_proofs
> "/home/robert/Project/laholide/opentheory/natural-divides.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/natural-divides.art at
> line 159: defineConst\nstack = [Term; \"Number.Natural.divides\"; Var; Var;
> []]\nunknown constant \"Number.Natural.divides\"".
> # let p = load_proofs
> "/home/robert/Project/laholide/opentheory/modular.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/modular.art at line
> 155: const\nstack = [\"Number.Modular.modulus\"; Term; Term; Var; Var;
> \"Number.Modular.equivalent\"; Term; Var; Term; Var; [];
> \"HOLLight.modular_to_class\"; \"HOLLight.modular_from_class\";
> \"Number.Modular.modular\"; TypeOp<fun>; TypeOp<fun>; Const<!>]\nunknown
> constant \"Number.Modular.modulus\"".
> # let p = load_proofs "/home/robert/Project/laholide/opentheory/gfp.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/gfp.art at line 54:
> const\nstack = [\"Number.GF(p).oddprime\"; Term; Var; []]\nunknown constant
> \"Number.GF(p).oddprime\"".
> # let p = load_proofs
> "/home/robert/Project/laholide/opentheory/natural-fibonacci.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/natural-fibonacci.art
> at line 1933: defineConstList\nstack = [Thm;
> [[\"Number.Natural.Fibonacci.zeckendorf\"; Var]]; Var; []; Thm]\nunknown
> constant \"Number.Natural.Fibonacci.zeckendorf\"".
> # let p = load_proofs "/home/robert/Project/laholide/opentheory/word.art";;
> Exception:
> Failure
>  "in article /home/robert/Project/laholide/opentheory/word.art at line 130:
> const\nstack = [\"Data.Word.width\"; Term; \"Data.Word.modulus\"; Thm;
> Thm]\nunknown constant \"Data.Word.width\"".
> #
>
> Could you please help on that? It seems I can't even play with the other
> article files I used to be able to load either :(
>
> Thanks very much!
>
> --
>
> Regards,
> Robert White (Shuai Wang)
> INRIA Deducteam
> [Moving to ILLC of UvA from this Sep to continue my masters. ]
> [New email address will be shuai.wang at student.uva.nl]
>