[opentheory-users] extending the standard library

[Ramana Kumar]

Hi Joe,

Sorry for the long delay. I think I agree with what you've said so far.

My next questions are about how, practically, to extend the standard
library.

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?

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?

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?

[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?]

~

On 14 May 2016 at 04:22, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> Thanks for taking the time to synchronize the discussion.
>
> > On creating theories in the HOL4 namespace, and depending on the hol-base
> > package: I see these as interim measures, with my desired goal being that
> > the
> > theorems and additional constants eventually all make it into the
> standard
> > namespace and depend on a nicely organised, unified, tree of packages. I
> > think
> > we probably agree on that goal, but I'm not sure. What do you say?
>
> Yes, I agree. I see the HOL4 namespace and the hol-base package as a
> convenient place to put HOL4-specific theories while we decide what
> will be the highest value to port to the "nicely organised, unified,
> tree of packages" depending only on the standard theory library.
>
> > More generally, my goal is to put together OpenTheory packages that are
> so
> > compelling in their organisation and coverage, having taken theorems from
> > all
> > the existing HOL provers, that everyone wants to use them. I want to move
> > towards unification and away from fragmentation. I would be sad if
> > OpenTheory
> > simply becomes a mirror of the existing fragmentation and incompatibility
> > between the various theorem prover libraries today. Do you agree with
> this
> > more
> > general goal?
>
> Agreed also, which is somewhat motivating my resistance to including
> totalized constants (see below).
>
> > I would like to discuss how to achieve the HOL4-specific goal now,
> because I
> > think we have enough information to make progress on such a discussion
> > (enough
> > HOL4 packages are already created). (This is in response to "When the
> HOL4
> > theory packages are in place...".)
>
> OK sure, let's now discuss moving HOL4 packages away from their
> holding station in the HOL4 namespace depending on the hol-base
> package.
>
> > Now back to the questions from my previous email:
> >
> >  - Do you agree with the three pieces of my solution to issue (2)? How do
> > you
> >    think responsibility for those tasks should be divided between readers
> > and
> >    creators?
>
> For issue (2) I was only considering the case where native and
> OpenTheory constants have different but isomorphic types, such as zip
> which might be defined as either of
>
> A list * B list -> (A * B) list
> A list -> B list -> (A * B) list
>
> If this is the only difference we can provide an unconditional
> equation between the OpenTheory and native variants of these
> constants. I agree with your three pieces of the solution, and I would
> hope that the theory creator could handle all of them so the reader
> would not have to know about the native constant with the different
> type.
>
> Actually, this is not strictly true, since reading such a theory might
> involve defining the HOL4 variant of the constant (just as reading the
> real theory involves defining some symbols in the HOLLight namespace),
> but I am ok with generating a bit of name pollution in logical kernels
> that are not purely functional. [This can already happen when
> auxiliary definitions are made to support definitions and proofs.]
>
> >  - I guess your response "I'm loath to totalize any of the constants..."
> was
> >    mainly to my suggested solution 0 to issue (3). That is a reasonable
> >    objection to solution 0.
> >    But:
> >    What do you think of solution 1, namely, providing multiple versions
> of
> >    constants that can be overspecified (in addition to the underspecified
> >    version), together with theorems relating them?
>
> I've thought a lot about this, and am still not sure about adding
> totalized constants to OpenTheory theories that are intended to be
> read into arbitrary environments. For a concrete case, let's consider
> defining the HOL4 real inverse function:
>
> |- !x. inv0 x = if x = 0 then 0 else inv 0
>
> This makes it clear that when the argument can be proved to be
> non-zero, then inv0 and inv are interchangeable.
>
> The problem is that if I add inv0 to the real theory, then it has no
> binding in an environment that doesn't contain that totalized
> constant. And similarly the theorems about inv0, such as
>
> |- inv0 0 = 0
>
> don't have any equivalents in this environment. So we'd essentially be
> asking this environment to define inv0 and prove these theorems,
> because they'd be used in the proof of other theorems not involving
> inv0.
>
> In general each environment would have to define each variant of
> totalized constants, and maintain them as visible symbols with
> searchable theorems about them.
>
> The alternative I'd prefer would be for the native symbols to be
> hidden inside theories (HOL4.inv instead of inv0), just as in the case
> of native symbols with different types, which would require their
> properties to be proved each time inside theories that use them
> instead of being proved once and exported (static linking instead of
> dynamic linking).
>
> This focus on minimizing the work of the reader admittedly maximizes
> the burden on theory creators, but at least it avoids each environment
> needing to define and maintain properties of constant variants from
> other environments. In the extreme case of purely functional logical
> kernels then variants of constants from other environments just exist
> transiently to support proofs and are otherwise completely invisible.
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20161005/12f3cf89/attachment.html>