[opentheory-users] extending the standard library

[Joe Leslie-Hurd]

Hi Ramana,

Thank you for picking up this discussion.

> Consider a mostly unproblematic constant like HOL4.list.GENLIST. Suppose I
> want this constant and various theorems about it to become part of the
> standard library. Is the idea to produce list-tabulate-def and
> list-tabulate-thm packages that could be included in list (and thereby
> base)? If someone produced suitable packages with a new constant, would you
> add them?

My intention has always been that the standard theory library (i.e.,
base) contains only what you could expect to find in every HOL theorem
prover, and provides enough to build interesting theories on top of
it. Thus each theorem prover could bind the standard theory library to
its own environment and then it would be able to load all the theories
stored in an OpenTheory repo.

So with this philosophy the your GENLIST constant would start off life
in some theory (not base) uploaded to an OpenTheory repo, whereupon it
could be loaded into any HOL theorem prover. If one day we discover
that every HOL theorem prover has incorporated it into its core
distribution, then it could be moved into the list theory (and
therefore also base).

> Suppose I want to add more theorems about existing constants. Then the
> package doesn't have a natural name, something like list-extra (and then
> list-extra-more ...) - but I suppose I can just provide the article, and you
> can add it to the list package directly?

If you think the omission of the theorems from the standard theory
library is an error then I'd be happy to find a way to add them, but
if they are just extra theorems about existing constants then perhaps
they should go into a new theory as per the GENLIST example above.

> What would be useful is infrastructure for manipulating theories, e.g.,
> alpha-renaming theorems, or splitting their conjuncts, or whatever stylistic
> tweaks you want, or removing exported theorems... all after they have been
> recorded, at the OpenTheory stage, and without requiring lots of long
> replaying of articles. I don't suppose you have anything like this?

Sorry, I don't. The opentheory tool is a command-line tool now and for
the foreseeable future, and the operations you describe seem more
easily handled by a read-eval-print-loop like the one inside a theorem
prover.

> [I also worry that it's a lot of work to build the library and any
> infrastructure, and it might go to waste if there's not enough buy-in. For
> example, will there ever be buy-in from people who want type classes, or
> dependent types, or who do not want the axiom of choice or function
> extensionality, unless OpenTheory (and its standard library) somehow support
> all those things?  ... Is there anyone else on this list who would want to
> see the standard library developed and extended?]

I agree that there is a lot of engineering work that could be done to
improve the infrastructure if there was sufficient interest in
OpenTheory packages as a unit of exchange between HOL theorem provers.
Until that interest appears I wouldn't recommend investing the effort
(but of course the interest may not manifest until the infrastructure
is more mature, creating a Catch-22 situation :-).

Cheers,

Joe